proposition: Lemma disaster2 : 1 === 2 -> False.
proof: Proof. Admitted. Lemma rewrite_is_fun T (f : T -> T -> T) (a b c : T): commutative f -> associative f -> f (f b a) c = f a (f c b). Proof. Admitted. Lemma max_l m n: n <= m -> maxn m n = m. Proof. Admitted. Lemma succ_max_distr_r n m : (maxn n m).+1 = maxn (n.+1) (m.+1). Proof. Admitted. Lemma plus_max_distr_l m n p: maxn (p + n) (p + m) = p + maxn n m. Proof. Admitted. Inductive nat_rels m n : bool -> bool -> bool -> Set := | CompareNatLt of m < n : nat_rels m n true false false | CompareNatGt of m > n : nat_rels m n false true false | CompareNatEq of m = n : nat_rels m n false false true. Lemma natrelP m n : nat_rels m n (m < n) (n < m) (m == n). Proof. rewrite ltn_neqAle eqn_leq; case: ltnP; first by constructor. by rewrite leq_eqVlt orbC; case: leqP; constructor; first exact/eqnP. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool)