proposition: Lemma max_is_max m n: n <= maxn m n /\ m <= maxn m n.
proof: Proof. Abort. Inductive leq_xor_gtn m n : bool -> bool -> Set := | LeqNotGtn of m <= n : leq_xor_gtn m n true false | GtnNotLeq of n < m : leq_xor_gtn m n false true. Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m). Proof. rewrite ltnNge. by case X: (m <= n); constructor=>//; rewrite ltnNge X. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool)