Commit f9fecd84 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

pred_max migrated in Utils.v

parent b7c1081f
......@@ -374,6 +374,12 @@ Proof.
omega with *.
Qed.
Lemma pred_max a b :
Nat.pred (Nat.max a b) = Nat.max (Nat.pred a) (Nat.pred b).
Proof.
symmetry. apply Nat.max_monotone. red. red. auto with *.
Qed.
Lemma list_max_le l p :
list_max l <= p <-> (forall n, In n l -> n <= p).
Proof.
......
......@@ -122,12 +122,6 @@ Definition IsAx A :=
check ZFSign B = true /\
FClosed B).
Lemma pred_max a b :
Nat.pred (Nat.max a b) = Nat.max (Nat.pred a) (Nat.pred b).
Proof.
symmetry. apply Nat.max_monotone. red. red. auto with *.
Qed.
Lemma WCAx A : IsAx A -> WC ZFSign A.
Proof.
intros [ IN | [ (B & -> & HB & HB') | (C & -> & HC & HC') ] ].
......
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