proposition: Theorem pfact3 : Pfact 3 6.
proof: Proof. apply Pfact1 with (n := 3)(v := 2). discriminate. apply (Pfact1 2 1). discriminate. apply (Pfact1 1 1). discriminate. apply Pfact0. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector