|
(** ROmega is now aware of the bodies of context variables
(of type Z or nat).
See also #148 for the corresponding improvement in Omega.
*)
Require Import ZArith Lia.
Open Scope Z.
Goal let x := 3 in x = 3.
intros.
lia.
Qed.
(** Example seen in #4132
(actually solvable even if b isn't known to be 5) *)
Lemma foo
(x y x' zxy zxy' z : Z)
(b := 5)
(Ry : - b <= y < b)
(Bx : x' <= b)
(H : - zxy' <= zxy)
(H' : zxy' <= x') : - b <= zxy.
Proof.
lia.
Qed.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
