theorem proved term proof

`classC_count`

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

formal statement (Lean)

 146theorem classC_count :
 147    (allPowers.filter (fun p => powerClass p == .NautilusClass)).length = 6 := by native_decide

Term-mode proof.

 148
 149/-- Class D has exactly 5 powers. -/

Lean names referenced from this declaration's body.