Let z be given.
Assume Hz.
Set x to be the term Re z.
Set y to be the term Im z.
Set gamma to be the term
(sqrt_SNo_nonneg (eps_ 1 * (x + modulus_CSNo z))).
Set delta to be the term
(sqrt_SNo_nonneg (eps_ 1 * (- x + modulus_CSNo z))).
We will
prove (if y < 0 ∨ y = 0 ∧ x < 0 then pa gamma (- delta) else pa gamma delta)2 = z.
We prove the intermediate claim Lx: SNo x.
An
exact proof term for the current goal is
CSNo_ReR z Hz.
We prove the intermediate claim Ly: SNo y.
An
exact proof term for the current goal is
CSNo_ImR z Hz.
We prove the intermediate
claim Lmx:
SNo (- x).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Lx.
We prove the intermediate
claim Lmy:
SNo (- y).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Ly.
We prove the intermediate
claim Lx2S:
SNo (x ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat x Lx 2 nat_2.
We prove the intermediate
claim Ly2S:
SNo (y ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat y Ly 2 nat_2.
We prove the intermediate
claim Lx2nn:
0 ≤ x ^ 2.
rewrite the current goal using exp_SNo_nat_2 x Lx (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg x Lx.
We prove the intermediate
claim Ly2nn:
0 ≤ y ^ 2.
rewrite the current goal using exp_SNo_nat_2 y Ly (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg y Ly.
We prove the intermediate
claim Lx2mx2:
x ^ 2 = (- x) ^ 2.
rewrite the current goal using exp_SNo_nat_2 x Lx (from left to right).
rewrite the current goal using
exp_SNo_nat_2 (- x) Lmx (from left to right).
We will
prove x * x = (- x) * (- x).
Use symmetry.
An exact proof term for the current goal is mul_SNo_minus_minus x x Lx Lx.
We prove the intermediate
claim Lsx2S:
SNo (sqrt_SNo_nonneg (x ^ 2)).
An
exact proof term for the current goal is
SNo_sqrt_SNo_nonneg (x ^ 2) ?? ??.
We prove the intermediate
claim Lsx2nn:
0 ≤ sqrt_SNo_nonneg (x ^ 2).
An
exact proof term for the current goal is
sqrt_SNo_nonneg_nonneg (x ^ 2) ?? ??.
We prove the intermediate
claim Lsy2S:
SNo (sqrt_SNo_nonneg (y ^ 2)).
An
exact proof term for the current goal is
SNo_sqrt_SNo_nonneg (y ^ 2) ?? ??.
We will
prove x ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
Apply SNoLe_tra x (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2 + y ^ 2)) Lx ?? ?? to the current goal.
We will
prove x ≤ sqrt_SNo_nonneg (x ^ 2).
Apply SNoLtLe_or x 0 Lx SNo_0 to the current goal.
Assume H1: x < 0.
Apply SNoLe_tra x 0 (sqrt_SNo_nonneg (x ^ 2)) Lx SNo_0 ?? to the current goal.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H1.
We will
prove 0 ≤ sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is Lsx2nn.
Assume H1: 0 ≤ x.
Apply SNoLe_ref to the current goal.
We will
prove sqrt_SNo_nonneg (x ^ 2) ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We will
prove x ^ 2 ≤ x ^ 2 + y ^ 2.
rewrite the current goal using
add_SNo_0R (x ^ 2) ?? (from right to left) at position 1.
We will
prove x ^ 2 + 0 ≤ x ^ 2 + y ^ 2.
Apply add_SNo_Le2 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is SNo_0.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We will
prove - x ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
Apply SNoLe_tra (- x) (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2 + y ^ 2)) Lmx ?? ?? to the current goal.
We will
prove - x ≤ sqrt_SNo_nonneg (x ^ 2).
Apply SNoLtLe_or (- x) 0 Lmx SNo_0 to the current goal.
Apply SNoLe_tra (- x) 0 (sqrt_SNo_nonneg (x ^ 2)) Lmx SNo_0 ?? to the current goal.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H1.
We will
prove 0 ≤ sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is Lsx2nn.
rewrite the current goal using Lx2mx2 (from left to right).
Apply SNoLe_ref to the current goal.
We will
prove sqrt_SNo_nonneg (x ^ 2) ≤ sqrt_SNo_nonneg (x ^ 2 + y ^ 2).
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We will
prove x ^ 2 ≤ x ^ 2 + y ^ 2.
rewrite the current goal using
add_SNo_0R (x ^ 2) ?? (from right to left) at position 1.
We will
prove x ^ 2 + 0 ≤ x ^ 2 + y ^ 2.
Apply add_SNo_Le2 to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is SNo_0.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is ??.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Le1S: SNo (eps_ 1).
An exact proof term for the current goal is SNo_eps_ 1 (nat_p_omega 1 nat_1).
We prove the intermediate claim Le1nn: 0 ≤ eps_ 1.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos 1 (nat_p_omega 1 nat_1).
We prove the intermediate
claim Le12S:
SNo (eps_ 1 ^ 2).
Apply SNo_exp_SNo_nat to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is nat_2.
We prove the intermediate
claim Le12nn:
0 ≤ eps_ 1 ^ 2.
rewrite the current goal using exp_SNo_nat_2 (eps_ 1) ?? (from left to right).
Apply mul_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim Le1aS:
SNo (eps_ 1 * (x + modulus_CSNo z)).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
rewrite the current goal using
add_SNo_com x (modulus_CSNo z) ?? ?? (from left to right).
rewrite the current goal using minus_SNo_invol x Lx (from right to left).
Apply add_SNo_minus_Le2b (modulus_CSNo z) (- x) 0 ?? Lmx SNo_0 to the current goal.
rewrite the current goal using
add_SNo_0L (- x) Lmx (from left to right).
An exact proof term for the current goal is Lmgtnx.
We prove the intermediate
claim Le1ann:
0 ≤ eps_ 1 * (x + modulus_CSNo z).
Apply mul_SNo_nonneg_nonneg (eps_ 1) (x + modulus_CSNo z) to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim Le1maS:
SNo (eps_ 1 * (- x + modulus_CSNo z)).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
rewrite the current goal using
add_SNo_com (- x) (modulus_CSNo z) ?? ?? (from left to right).
Apply add_SNo_minus_Le2b (modulus_CSNo z) x 0 ?? Lx SNo_0 to the current goal.
rewrite the current goal using add_SNo_0L x Lx (from left to right).
An exact proof term for the current goal is Lmgtx.
We prove the intermediate
claim Le1mann:
0 ≤ eps_ 1 * (- x + modulus_CSNo z).
Apply mul_SNo_nonneg_nonneg (eps_ 1) (- x + modulus_CSNo z) to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply mul_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LgammaS: SNo gamma.
Apply SNo_sqrt_SNo_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lgammann: 0 ≤ gamma.
Apply sqrt_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LdeltaS: SNo delta.
Apply SNo_sqrt_SNo_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Ldeltann: 0 ≤ delta.
Apply sqrt_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim LmdeltaS:
SNo (- delta).
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate
claim LdeltagammaS:
SNo (delta * gamma).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim Lpa1:
CSNo (pa gamma (- delta)).
Apply CSNo_I to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim Lpa2:
CSNo (pa gamma delta).
Apply CSNo_I to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate
claim Lpa1s:
CSNo (pa gamma (- delta)2).
An exact proof term for the current goal is ??.
An exact proof term for the current goal is nat_2.
We prove the intermediate
claim Lpa2s:
CSNo (pa gamma delta2).
An exact proof term for the current goal is ??.
An exact proof term for the current goal is nat_2.
We prove the intermediate
claim Lgamma2eq:
gamma * gamma = eps_ 1 * (x + modulus_CSNo z).
An
exact proof term for the current goal is
sqrt_SNo_nonneg_sqr (eps_ 1 * (x + modulus_CSNo z)) ?? ??.
We prove the intermediate
claim Ldelta2eq:
delta * delta = eps_ 1 * (- x + modulus_CSNo z).
An
exact proof term for the current goal is
sqrt_SNo_nonneg_sqr (eps_ 1 * (- x + modulus_CSNo z)) ?? ??.
We prove the intermediate
claim Ldeltagamma:
delta * gamma = eps_ 1 * sqrt_SNo_nonneg (y ^ 2).
rewrite the current goal using
mul_SNo_com_4_inner_mid (eps_ 1) (- x + modulus_CSNo z) (eps_ 1) (x + modulus_CSNo z) ?? ?? ?? ?? (from left to right).
rewrite the current goal using exp_SNo_nat_2 (eps_ 1) ?? (from right to left).
Use f_equal.
Use f_equal.
rewrite the current goal using
mul_SNo_minus_distrL x (modulus_CSNo z) ?? ?? (from left to right).
rewrite the current goal using
mul_SNo_com (modulus_CSNo z) x ?? ?? (from left to right).
rewrite the current goal using
sqrt_SNo_nonneg_sqr (abs_sqr_CSNo z) ?? ?? (from left to right).
We will
prove (- x) * x + x ^ 2 + y ^ 2 = y ^ 2.
Apply mul_SNo_minus_distrL x x ?? ?? (λ_ v ⇒ v + x ^ 2 + y ^ 2 = y ^ 2) to the current goal.
rewrite the current goal using exp_SNo_nat_2 x ?? (from right to left).
We will
prove - x ^ 2 + x ^ 2 + y ^ 2 = y ^ 2.
An
exact proof term for the current goal is
add_SNo_minus_L2 (x ^ 2) (y ^ 2) ?? ??.
We prove the intermediate
claim Lgamma2mdelta2:
gamma * gamma + - (delta * delta) = x.
rewrite the current goal using Lgamma2eq (from left to right).
rewrite the current goal using Ldelta2eq (from left to right).
rewrite the current goal using
mul_SNo_minus_distrR (eps_ 1) (- x + modulus_CSNo z) ?? ?? (from right to left).
rewrite the current goal using
minus_add_SNo_distr (- x) (modulus_CSNo z) ?? ?? (from left to right).
rewrite the current goal using minus_SNo_invol x ?? (from left to right).
rewrite the current goal using
add_SNo_com_4_inner_mid x (modulus_CSNo z) x (- modulus_CSNo z) ?? ?? ?? ?? (from left to right).
rewrite the current goal using
add_SNo_minus_SNo_rinv (modulus_CSNo z) ?? (from left to right).
We will
prove eps_ 1 * ((x + x) + 0) = x.
rewrite the current goal using
add_SNo_0R (x + x) (SNo_add_SNo x x ?? ??) (from left to right).
We will
prove eps_ 1 * (x + x) = x.
rewrite the current goal using mul_SNo_distrL (eps_ 1) x x ?? ?? ?? (from left to right).
We will
prove eps_ 1 * x + eps_ 1 * x = x.
rewrite the current goal using mul_SNo_distrR (eps_ 1) (eps_ 1) x ?? ?? ?? (from right to left).
We will
prove (eps_ 1 + eps_ 1) * x = x.
rewrite the current goal using eps_1_half_eq1 (from left to right).
An exact proof term for the current goal is mul_SNo_oneL x ??.
Apply SNoLt_trichotomy_or_impred y 0 Ly SNo_0 to the current goal.
Assume H1: y < 0.
We prove the intermediate claim Lcase1cond: y < 0 ∨ y = 0 ∧ x < 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
rewrite the current goal using
If_i_1 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase1cond (from left to right).
We will
prove pa gamma (- delta)2 = z.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will
prove Re (pa gamma (- delta) ⨯ pa gamma (- delta)) = x.
rewrite the current goal using
mul_CSNo_CRe (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will
prove gamma * gamma + - ((- delta) * (- delta)) = x.
rewrite the current goal using mul_SNo_minus_minus delta delta ?? ?? (from left to right).
We will
prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will
prove Im (pa gamma (- delta) ⨯ pa gamma (- delta)) = y.
rewrite the current goal using
mul_CSNo_CIm (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will
prove (- delta) * gamma + (- delta) * gamma = y.
rewrite the current goal using mul_SNo_minus_distrL delta gamma ?? ?? (from left to right).
We will
prove - delta * gamma + - delta * gamma = y.
rewrite the current goal using
minus_add_SNo_distr (delta * gamma) (delta * gamma) ?? ?? (from right to left).
We will
prove - (delta * gamma + delta * gamma) = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will
prove - (eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + eps_ 1 * sqrt_SNo_nonneg (y ^ 2)) = y.
rewrite the current goal using
mul_SNo_distrR (eps_ 1) (eps_ 1) (sqrt_SNo_nonneg (y ^ 2)) ?? ?? ?? (from right to left).
rewrite the current goal using eps_1_half_eq1 (from left to right).
rewrite the current goal using
mul_SNo_oneL (sqrt_SNo_nonneg (y ^ 2)) ?? (from left to right).
We will
prove - sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using exp_SNo_nat_2 y ?? (from left to right).
We will
prove - sqrt_SNo_nonneg (y * y) = y.
rewrite the current goal using mul_SNo_minus_minus y y ?? ?? (from right to left).
We will
prove - sqrt_SNo_nonneg ((- y) * (- y)) = y.
rewrite the current goal using
exp_SNo_nat_2 (- y) ?? (from right to left).
We will
prove - sqrt_SNo_nonneg ((- y) ^ 2) = y.
We prove the intermediate
claim L1:
0 ≤ - y.
Apply SNoLtLe to the current goal.
Apply minus_SNo_Lt_contra2 y 0 ?? SNo_0 to the current goal.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is minus_SNo_invol y ??.
Assume H1: y = 0.
Apply SNoLtLe_or x 0 Lx SNo_0 to the current goal.
Assume H2: x < 0.
We prove the intermediate claim Lcase1cond: y < 0 ∨ y = 0 ∧ x < 0.
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
rewrite the current goal using
If_i_1 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase1cond (from left to right).
We will
prove pa gamma (- delta)2 = z.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will
prove Re (pa gamma (- delta) ⨯ pa gamma (- delta)) = x.
rewrite the current goal using
mul_CSNo_CRe (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will
prove gamma * gamma + - ((- delta) * (- delta)) = x.
rewrite the current goal using mul_SNo_minus_minus delta delta ?? ?? (from left to right).
We will
prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma (- delta)) ?? (from left to right).
We will
prove Im (pa gamma (- delta) ⨯ pa gamma (- delta)) = y.
rewrite the current goal using
mul_CSNo_CIm (pa gamma (- delta)) (pa gamma (- delta)) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma (- delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma (- delta) ?? ?? (from left to right).
We will
prove (- delta) * gamma + (- delta) * gamma = y.
rewrite the current goal using mul_SNo_minus_distrL delta gamma ?? ?? (from left to right).
We will
prove - delta * gamma + - delta * gamma = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will
prove - eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + - eps_ 1 * sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using exp_SNo_nat_2 y ?? (from left to right).
rewrite the current goal using H1 (from left to right).
We will
prove - eps_ 1 * sqrt_SNo_nonneg (0 * 0) + - eps_ 1 * sqrt_SNo_nonneg (0 * 0) = 0.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).
We will
prove - eps_ 1 * 0 + - eps_ 1 * 0 = 0.
rewrite the current goal using mul_SNo_zeroR (eps_ 1) ?? (from left to right).
We will
prove - 0 + - 0 = 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
Assume H2: 0 ≤ x.
We prove the intermediate claim Lcase2cond: ¬ (y < 0 ∨ y = 0 ∧ x < 0).
Assume H.
Apply H to the current goal.
Assume H3: y < 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using H1 (from left to right) at position 2.
An exact proof term for the current goal is H3.
Assume H.
Apply H to the current goal.
Assume H3: y = 0.
Assume H4: x < 0.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
An exact proof term for the current goal is SNoLtLe_tra x 0 x ?? SNo_0 ?? H4 H2.
rewrite the current goal using
If_i_0 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase2cond (from left to right).
We will prove pa gamma delta2 = z.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will
prove Re (pa gamma delta ⨯ pa gamma delta) = x.
rewrite the current goal using
mul_CSNo_CRe (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will
prove Im (pa gamma delta ⨯ pa gamma delta) = y.
rewrite the current goal using
mul_CSNo_CIm (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove delta * gamma + delta * gamma = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will
prove eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + eps_ 1 * sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using exp_SNo_nat_2 y ?? (from left to right).
rewrite the current goal using H1 (from left to right).
We will
prove eps_ 1 * sqrt_SNo_nonneg (0 * 0) + eps_ 1 * sqrt_SNo_nonneg (0 * 0) = 0.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using sqrt_SNo_nonneg_0 (from left to right).
We will
prove eps_ 1 * 0 + eps_ 1 * 0 = 0.
rewrite the current goal using mul_SNo_zeroR (eps_ 1) ?? (from left to right).
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
Assume H1: 0 < y.
We prove the intermediate claim Lcase2cond: ¬ (y < 0 ∨ y = 0 ∧ x < 0).
Assume H.
Apply H to the current goal.
Assume H2: y < 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
An exact proof term for the current goal is SNoLt_tra y 0 y ?? SNo_0 ?? H2 H1.
Assume H.
Apply H to the current goal.
Assume H2: y = 0.
Assume H3: x < 0.
Apply SNoLt_irref y to the current goal.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is H1.
rewrite the current goal using
If_i_0 (y < 0 ∨ y = 0 ∧ x < 0) (pa gamma (- delta)) (pa gamma delta) Lcase2cond (from left to right).
We will prove pa gamma delta2 = z.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will
prove Re (pa gamma delta ⨯ pa gamma delta) = x.
rewrite the current goal using
mul_CSNo_CRe (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove gamma * gamma + - (delta * delta) = x.
An exact proof term for the current goal is Lgamma2mdelta2.
rewrite the current goal using
exp_CSNo_nat_2 (pa gamma delta) ?? (from left to right).
We will
prove Im (pa gamma delta ⨯ pa gamma delta) = y.
rewrite the current goal using
mul_CSNo_CIm (pa gamma delta) (pa gamma delta) ?? ?? (from left to right).
rewrite the current goal using
CSNo_Re2 gamma delta ?? ?? (from left to right).
rewrite the current goal using
CSNo_Im2 gamma delta ?? ?? (from left to right).
We will
prove delta * gamma + delta * gamma = y.
rewrite the current goal using Ldeltagamma (from left to right).
We will
prove eps_ 1 * sqrt_SNo_nonneg (y ^ 2) + eps_ 1 * sqrt_SNo_nonneg (y ^ 2) = y.
rewrite the current goal using
mul_SNo_distrR (eps_ 1) (eps_ 1) (sqrt_SNo_nonneg (y ^ 2)) ?? ?? ?? (from right to left).
rewrite the current goal using eps_1_half_eq1 (from left to right).
rewrite the current goal using
mul_SNo_oneL (sqrt_SNo_nonneg (y ^ 2)) ?? (from left to right).
We will
prove sqrt_SNo_nonneg (y ^ 2) = y.
We will prove 0 ≤ y.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H1.