| pf |
|---|
Apply nat_complete_ind with λ x0 . ∀ x1 . nat_p x1 ⟶ mul_SNo x0 x0 = mul_SNo 2 (mul_SNo x1 x1) ⟶ x1 = 0.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply SNoLeE with 0, x1, x1 = 0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L5.
Apply omega_nonneg with x1.
The subproof is completed by applying L4.
Apply FalseE with x1 = 0.
Apply SNoLt_irref with 0.
Apply H1 with div_SNo x0 2, div_SNo x1 2, λ x2 x3 . SNoLt 0 x2 leaving 4 subgoals.
Apply ordinal_SNoLt_In with div_SNo x0 2, x0 leaving 3 subgoals.
Apply nat_p_ordinal with div_SNo x0 2.
The subproof is completed by applying L13.
Apply nat_p_ordinal with x0.
The subproof is completed by applying H0.
Apply div_SNo_pos_LtL with x0, 2, x0 leaving 5 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying SNo_2.
The subproof is completed by applying L10.
The subproof is completed by applying SNoLt_0_2.
Apply add_SNo_Lt1_cancel with x0, minus_SNo x0, mul_SNo x0 2 leaving 4 subgoals.
The subproof is completed by applying L10.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying L10.
Apply SNo_mul_SNo with x0, 2 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying SNo_2.
Apply add_SNo_minus_SNo_rinv with x0, λ x2 x3 . SNoLt x3 (add_SNo (mul_SNo x0 2) (minus_SNo x0)) leaving 2 subgoals.
The subproof is completed by applying L10.
Apply mul_SNo_oneR with x0, λ x2 x3 . SNoLt 0 (add_SNo (mul_SNo x0 2) (minus_SNo x2)) leaving 2 subgoals.
The subproof is completed by applying L10.
Apply mul_SNo_minus_distrR with x0, 1, λ x2 x3 . SNoLt 0 (add_SNo (mul_SNo x0 2) x2) leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying SNo_1.
Apply mul_SNo_distrL with x0, 2, minus_SNo 1, λ x2 x3 . SNoLt 0 x2 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying SNo_2.
Apply SNo_minus_SNo with 1.
The subproof is completed by applying SNo_1.
Apply add_SNo_1_1_2 with λ x2 x3 . SNoLt 0 (mul_SNo x0 (add_SNo x2 (minus_SNo 1))).
Apply add_SNo_minus_R2 with 1, 1, λ x2 x3 . SNoLt 0 (mul_SNo x0 x3) leaving 3 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_1.
Apply mul_SNo_oneR with x0, λ x2 x3 . SNoLt 0 x3 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
Apply unknownprop_17e526dd107b435f5416528d1c977ef8aa1ea06ba09d8b9ed0ca53424a454f1a with div_SNo x1 2 leaving 2 subgoals.
Apply unknownprop_33dd36a008b55be6da4ee6635ff902fa41b5ac2488950386b58ffacb63ab031a with 2, x1.
Apply Euclid_lemma with 2, x1, x1, divides_int 2 x1 leaving 6 subgoals.
The subproof is completed by applying unknownprop_3729fc97c8b5f21188ac361733273781ed00775a9662ac2f2237f0346be243d1.
The subproof is completed by applying L7.
The subproof is completed by applying L7.
Apply and3I with 2 ∈ int, mul_SNo x1 x1 ∈ int, ∃ x2 . and (x2 ∈ int) (mul_SNo 2 x2 = mul_SNo x1 x1) leaving 3 subgoals.
Apply Subq_omega_int with 2.
Apply nat_p_omega with 2.
The subproof is completed by applying nat_2.
Apply int_mul_SNo with x1, x1 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L7.
Let x2 of type ο be given.
■ |
|