proposition: Lemma composite_prod_rev n: natp n -> composite n -> exists a b, [/\ natp a, natp b, \1c <c a, \1c <c b & n = a *c b].
proof: Proof. move => nN [a [aN pa pb pc]]; exists a,(n %/c a). move:(cdivides_pr pc) (NS_quo a nN) => eq qN; rewrite - eq; split => //;split. rewrite - succ_zero; apply /(cleSltP NS0); split; first exact:(cle0n qN). move => qz. by case:(proj2 (clt_ltT clt_01 (clt_ltT pa pb))); rewrite eq - qz cprod0r. by move => eq1;move: (proj2 pb);rewrite eq - eq1 (cprod1r (CS_nat aN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)