proposition: Lemma MAX_def : max = (fun _2273 : nat => fun _2274 : nat => @COND nat (Peano.le _2273 _2274) _2274 _2273).
proof: Proof. apply fun_ext; intro x. apply fun_ext. induction x; intro y; induction y. rewrite _0_le_nat_is_True, COND_True. reflexivity. simpl. rewrite _0_le_nat_is_True, COND_True. reflexivity. rewrite S_le_0_is_False, COND_False. reflexivity. simpl. rewrite IHx, S_le_S. destruct (prop_degen (x <= y)) as [h|h]; rewrite h. rewrite! COND_True. reflexivity. rewrite! COND_False. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat