Exact expanded PA statement
forall n k. S n = 2 * k -> (~(k = 0) /\ (exists bcf_le_gap_bdhpb_result. bcf_le_gap_bdhpb_result + (k) = n))Structural proof guide
An even successor has a nonzero half below its predecessor.
Direct prerequisites: two_mul_eq_add_self, add_succ_left. The authored body proceeds by structural induction (1), closed numeral normalization (1).
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.