proposition: Lemma ffact_ge0 (n : int) (m : nat) : n >= 0 -> 0 <= n ^_ m.
proof: Proof. case: n => n //. elim: n m => [ | n ihn] m _; first by rewrite ffact0n. case: m ihn => [ | m] ihn; first by rewrite ffactn0. by rewrite ffactnS subzSS subr0 pmulr_rge0 // ihn. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics