Commit f7fe2229 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Added Zgt_not_eq.

parent 1e62a8e6
......@@ -317,6 +317,15 @@ apply Zplus_le_reg_r with (-x - y)%Z.
now ring_simplify.
Qed.
Theorem Zgt_not_eq :
forall x y : Z,
(y < x)%Z -> (x <> y)%Z.
Proof.
intros x y H Hn.
apply Zlt_irrefl with x.
now rewrite Hn at 1.
Qed.
Theorem Zmin_left :
forall x y : Z,
(x <= y)%Z -> Zmin x y = x.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment