Erdos769.erdos769_lower_bound_false : ¬Erdos769.Erdos769LowerBound
'Erdos769.erdos769_lower_bound_false' depends on axioms: [propext, Classical.choice, Quot.sound]
PASS: canonical Erdős 769 lower-bound proposition disproved by Lean with no sorry/admit/custom axioms
