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