proposition: Lemma ffact_gt0 (n : int) (m : nat) : n >= 0 -> (0 < n ^_ m) = (Posz m <= n).
proof: Proof. case: n => // n _; elim: n m => [ | n IHn] [ | m] //=. by rewrite ffact0n /= lez0_nat. by rewrite ffactnS subzSS subr0 pmulr_rgt0 // IHn. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics