proposition: Lemma NleT a b c: a <=N b -> b <=N c -> a <=N c.
proof: Proof. move /Nat_order_leP => ab /Nat_order_leP bc; apply /Nat_order_leP. move: Nat_order_wor=> [[or wor] _]; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)