proposition: Theorem Zle_Pfact : forall x:Z, 0 <= x -> exists y:Z, Pfact x y.
proof: Proof. intros x; induction x using (well_founded_ind (Zwf_well_founded 0)). intros Hle; destruct (Zle_lt_or_eq _ _ Hle). - destruct (H (x-1)). + unfold Zwf; lia. + lia. + exists (x*x0); apply Pfact1; auto with zarith. - subst x; exists 1; constructor. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector