proposition: Lemma maxn_idPl_bis m n : reflect (maxn m n = m) (m >= n).
proof: Proof. End easy. Module reflect1. Inductive reflectl (P : Prop) b := | RT (p : P) (e : b = true) | RF (p : ~ P) (e : b = false). About reflect. Lemma andP (b1 b2 : bool) : reflectl (b1 /\ b2) (b1 && b2). Proof. Qed.
imports: mathcomp(all_ssreflect)