proposition: Lemma ltnP m n : ltn_xor_geq m n (minn n m) (minn m n) (maxn n m) (maxn m n) (n <= m) (m < n).
proof: Proof. by case: leqP; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring