proposition: Lemma T1leP x y : T1leq_xor_gtn x y (x <= y) (y < x).
proof: Proof. by rewrite T1ltNge; case le_xy: (x <= y); constructor;rewrite // T1ltNge le_xy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)