proposition: Lemma leq_pfact : {in [pred n | 0 < n] &, {mono factorial : m n / m <= n}}.
proof: Proof. by apply: leq_mono_in => n m n0 m0; apply: ltn_fact. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring