proposition: Lemma leqifP m n C : reflect (m <= n ?= iff C) (if C then m == n else m < n).
proof: Proof. rewrite ltn_neqAle; apply: (iffP idP) => [|lte]; last by rewrite !lte; case C. by case C => [/eqP-> | /andP[/negPf]]; split=> //; apply: eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring