proposition: Lemma leqP m n : leq_xor_gtn m n (minn n m) (minn m n) (maxn n m) (maxn m n) (m <= n) (n < m).
proof: Proof. rewrite (minnC m) /minn (maxnC m) /maxn ltnNge. by case le_mn: (m <= n); constructor; rewrite //= ltnNge le_mn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring