proposition: Lemma leq_max m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2).
proof: Proof. case/orP: (leq_total n2 n1) => [le_n21 | le_n12]. Abort. Print Bool.reflect. About andP. Lemma example_spec a b : a && b ==> (a == b). Proof. by case: andP => [ [-> ->] | // ]. Qed.
imports: mathcomp(all_ssreflect)