|
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.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
