proposition: Lemma ffact_small (n m : nat) : Posz n < Posz m -> n ^_ m = 0.
proof: Proof. move=> hnm; apply/eqP; rewrite eq_le ffact_ge0 // leNgt ffact_gt0 //. by rewrite -ltNge andbT. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics