proposition: Lemma ltngtP m n : compare_nat m n (minn n m) (minn m n) (maxn n m) (maxn m n) (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n).
proof: Proof. rewrite !ltn_neqAle [_ == n]eq_sym; have [mn|] := ltnP m n. by rewrite ltnW // gtn_eqF //; constructor. rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_nm eq_nm. by rewrite ltn_eqF //; constructor. by rewrite eq_nm (eqP eq_nm); constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring