proposition: Lemma composite_prod a b: natp a -> natp b -> \1c <c a -> \1c <c b -> composite (a *c b).
proof: Proof. move => aN bN h1 h2. move/(strict_pos_P1 aN): (clt_ltT clt_01 h1) => anz. by exists a;split => //; [apply:cprod_M1lt | apply: cdivides_pr1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)