n : 0 < n -> factorial n < factorial n.+1. Proof. intro H. rewrite <- (nat_mul_one_l (factorial n)). rapply (nat_mul_r_strictly_monotone _). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids