proposition: Lemma leP m n : reflect (m <= n)%coq_nat (m <= n).
proof: Proof. apply: (iffP idP); last by elim: n / => // n _ /leq_trans->. elim: n => [|n IHn]; first by case: m. by rewrite leq_eqVlt ltnS => /predU1P[<- // | /IHn]; right. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring