Commit ac178ce2 authored by Martin PORTALIER's avatar Martin PORTALIER

Update facts.v

parent 1d0a26de
Pipeline #19190 failed with stages
in 51 seconds
......@@ -10,6 +10,12 @@ Require Import List Classical_Prop Classical_Pred_Type.
move => m n H_pos H_sup. ssromega.
Qed.
Lemma lt1_leq : forall m n,
m < n -> m + 1 <= n.
Proof.
move => m n H_inf. ssromega.
Qed.
Lemma neq_sym: forall (n m : nat),
(n != m) = (m != n).
Proof.
......
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