Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_4701.v Sprache: Cobol

Original von: Coq^©

Require Import Ring.
Require Import ArithRing.

Ltac ring_simplify_neq :=
  match goal with
  | [ H: ?X <> ?Y |- _ ] => progress ring_simplify X Y in H
  end.

Lemma toto : forall x y, x*1 <> y*1 -> y*1 <> x*1 -> x<>y.
Proof.
  intros.
  ring_simplify_neq.
  ring_simplify_neq.
  (* make sure ring_simplify has simplified both hypotheses *)
  match goal with
  | [ H: context[_*1] |- _ ] => fail 1
  | _ => idtac
  end.
  auto.
Qed.

¤ Dauer der Verarbeitung: 0.52 Sekunden (vorverarbeitet) ¤

Kontakt Drucken
Kontakt sprechenden Kalenders
Eigene Datei ansehen

schauen Sie vor die Tür

Fenster

Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.