proposition: Lemma maxnE m n : maxn m n = m + (n - m).
proof: Proof. rewrite /maxn; elim: m n => [|m ih] [|n]; rewrite ?addn0 //. by rewrite ltnS subSS addSn -ih; case: leq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring