proposition: Lemma segment_Nat_order1 n: natp n -> segment Nat_order n = n.
proof: Proof. by move=> nN; rewrite (segment_Nat_order nN) (NintE nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)