proposition: Lemma ltn_fact m n : 0 < m -> m < n -> m`! < n`!.
proof: Proof. case: m n => // m n _; elim: n m => // n ih [|m] ?; last by rewrite ltn_mul ?ih. by rewrite -[_.+1]muln1 leq_mul ?fact_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring