Commit caba5af6 authored by Martin PORTALIER's avatar Martin PORTALIER

Update facts.v

parent 13eebf56
Pipeline #19239 failed with stages
in 38 seconds
......@@ -16,7 +16,7 @@ Require Import List Classical_Prop Classical_Pred_Type.
move => m n H_inf. ssromega.
Qed.
Lemma neq_sym: forall (n m : nat),
Lemma neq_sym: forall (n m: nat),
(n != m) = (m != n).
Proof.
move => n m. apply /neqP/neqP; auto.
......
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