proposition: Lemma leq_fact : {homo factorial : m n / m <= n}.
proof: Proof. by move=> [m|m n mn]; rewrite ?fact_gt0// leq_pfact// inE (leq_trans _ mn). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring