theorem proved term proof

`vp_factorial_six_three`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 584theorem vp_factorial_six_three : vp 3 (Nat.factorial 6) = 2 := by native_decide

Term-mode proof.

 585
 586/-- vp 3 (9!) = 4. -/

Lean names referenced from this declaration's body.