Exact expanded PA statement
forall d n. (exists q. n = d * q) \/ ~(exists q. n = d * q)Structural proof guide
Divisibility of natural numbers is constructively decidable, including the zero divisor case.
Direct prerequisites: mul_zero_left, eq_decidable, multiple_decidable_nonzero. The authored body proceeds by case analysis (3), intermediate claims (2), equality transport (2).
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.
- 0001
intro d - 0002
intro n - 0003
specialize eq_decidable d - 0004
specialize eq_decidable 0 - 0005
have hd : d = 0 \/ ~(d = 0) - 0006
apply eq_decidable - 0007
cases hd - 0008
specialize eq_decidable_before n - 0009
specialize eq_decidable_before 0 - 0010
have hn : n = 0 \/ ~(n = 0) - 0011
apply eq_decidable_before - 0012
cases hn - 0013
left - 0014
exists 0 - 0015
trans 0 - 0016
exact hn_left - 0017
symm - 0018
rewrite hd_left - 0019
apply mul_zero_left - 0020
right - 0021
intro hmultiple - 0022
cases hmultiple - 0023
apply hn_right - 0024
trans d * x - 0025
exact hmultiple_witness - 0026
rewrite hd_left - 0027
apply mul_zero_left - 0028
apply multiple_decidable_nonzero - 0029
exact hd_right