Let c, y and z be given.
Assume HcR: c ∈ R.
Assume Hcpos: 0 < c.
Assume HyI: y ∈ closed_interval (add_SNo (minus_SNo 1) c) (add_SNo 1 (minus_SNo c)).
Assume HzI: z ∈ closed_interval (minus_SNo (mul_SNo c one_third)) (mul_SNo c one_third).
We will prove add_SNo y z ∈ closed_interval (add_SNo (minus_SNo 1) (mul_SNo c two_thirds)) (add_SNo 1 (minus_SNo (mul_SNo c two_thirds))).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim H13R: one_third ∈ R.
An exact proof term for the current goal is one_third_in_R.
We prove the intermediate claim H13S: SNo one_third.
An exact proof term for the current goal is (real_SNo one_third H13R).
We prove the intermediate claim H23R: two_thirds ∈ R.
An exact proof term for the current goal is two_thirds_in_R.
We prove the intermediate claim H23S: SNo two_thirds.
An exact proof term for the current goal is (real_SNo two_thirds H23R).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (add_SNo (minus_SNo 1) c) (add_SNo 1 (minus_SNo c)) y HyI).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim HzR: z ∈ R.
An exact proof term for the current goal is (closed_interval_sub_R (minus_SNo (mul_SNo c one_third)) (mul_SNo c one_third) z HzI).
We prove the intermediate claim HzS: SNo z.
An exact proof term for the current goal is (real_SNo z HzR).
We prove the intermediate claim Hc13R: mul_SNo c one_third ∈ R.
An exact proof term for the current goal is (real_mul_SNo c HcR one_third H13R).
We prove the intermediate claim Hc13S: SNo (mul_SNo c one_third).
An exact proof term for the current goal is (real_SNo (mul_SNo c one_third) Hc13R).
We prove the intermediate claim Hm_c13R: minus_SNo (mul_SNo c one_third) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo c one_third) Hc13R).
We prove the intermediate claim Hm_c13S: SNo (minus_SNo (mul_SNo c one_third)).
An exact proof term for the current goal is (SNo_minus_SNo (mul_SNo c one_third) Hc13S).
We prove the intermediate claim HmcR: minus_SNo c ∈ R.
An exact proof term for the current goal is (real_minus_SNo c HcR).
We prove the intermediate claim HmcS: SNo (minus_SNo c).
An exact proof term for the current goal is (SNo_minus_SNo c HcS).
We prove the intermediate claim Hc23R: mul_SNo c two_thirds ∈ R.
An exact proof term for the current goal is (real_mul_SNo c HcR two_thirds H23R).
We prove the intermediate claim Hc23S: SNo (mul_SNo c two_thirds).
An exact proof term for the current goal is (real_SNo (mul_SNo c two_thirds) Hc23R).
We prove the intermediate claim HyB: Rle (add_SNo (minus_SNo 1) c) y ∧ Rle y (add_SNo 1 (minus_SNo c)).
An exact proof term for the current goal is (closed_interval_bounds (add_SNo (minus_SNo 1) c) (add_SNo 1 (minus_SNo c)) y (real_add_SNo (minus_SNo 1) Hm1R c HcR) (real_add_SNo 1 real_1 (minus_SNo c) HmcR) HyI).
We prove the intermediate claim HyLo: Rle (add_SNo (minus_SNo 1) c) y.
An exact proof term for the current goal is (andEL (Rle (add_SNo (minus_SNo 1) c) y) (Rle y (add_SNo 1 (minus_SNo c))) HyB).
We prove the intermediate claim HyHi: Rle y (add_SNo 1 (minus_SNo c)).
An exact proof term for the current goal is (andER (Rle (add_SNo (minus_SNo 1) c) y) (Rle y (add_SNo 1 (minus_SNo c))) HyB).
We prove the intermediate claim HzB: Rle (minus_SNo (mul_SNo c one_third)) z ∧ Rle z (mul_SNo c one_third).
An exact proof term for the current goal is (closed_interval_bounds (minus_SNo (mul_SNo c one_third)) (mul_SNo c one_third) z Hm_c13R Hc13R HzI).
We prove the intermediate claim HzLo: Rle (minus_SNo (mul_SNo c one_third)) z.
An exact proof term for the current goal is (andEL (Rle (minus_SNo (mul_SNo c one_third)) z) (Rle z (mul_SNo c one_third)) HzB).
We prove the intermediate claim HzHi: Rle z (mul_SNo c one_third).
An exact proof term for the current goal is (andER (Rle (minus_SNo (mul_SNo c one_third)) z) (Rle z (mul_SNo c one_third)) HzB).
We prove the intermediate claim HsumR: add_SNo y z ∈ R.
An exact proof term for the current goal is (real_add_SNo y HyR z HzR).
We prove the intermediate claim HsumS: SNo (add_SNo y z).
An exact proof term for the current goal is (real_SNo (add_SNo y z) HsumR).
Set ylo to be the term add_SNo (minus_SNo 1) c.
Set zlo to be the term minus_SNo (mul_SNo c one_third).
We prove the intermediate claim HyloR: ylo ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo 1) Hm1R c HcR).
We prove the intermediate claim HyloS: SNo ylo.
An exact proof term for the current goal is (real_SNo ylo HyloR).
We prove the intermediate claim HzloR: zlo ∈ R.
An exact proof term for the current goal is Hm_c13R.
We prove the intermediate claim HzloS: SNo zlo.
An exact proof term for the current goal is Hm_c13S.
We prove the intermediate claim Hylzlo: Rle (add_SNo ylo zlo) (add_SNo ylo z).
An exact proof term for the current goal is (Rle_add_SNo_2 ylo zlo z HyloR HzloR HzR HzLo).
We prove the intermediate claim Hylz: Rle (add_SNo ylo z) (add_SNo y z).
An exact proof term for the current goal is (Rle_add_SNo_1 ylo y z HyloR HyR HzR HyLo).
We prove the intermediate claim Hylzlo2: Rle (add_SNo ylo zlo) (add_SNo y z).
An exact proof term for the current goal is (Rle_tra (add_SNo ylo zlo) (add_SNo ylo z) (add_SNo y z) Hylzlo Hylz).
We prove the intermediate claim Hylo_zlo_eq: add_SNo ylo zlo = add_SNo (minus_SNo 1) (mul_SNo c two_thirds).
We prove the intermediate claim HyloDef: ylo = add_SNo (minus_SNo 1) c.
Use reflexivity.
We prove the intermediate claim HzloDef: zlo = minus_SNo (mul_SNo c one_third).
Use reflexivity.
rewrite the current goal using HyloDef (from left to right).
rewrite the current goal using HzloDef (from left to right).
We prove the intermediate claim HcmulEq: add_SNo c (minus_SNo (mul_SNo c one_third)) = mul_SNo c two_thirds.
We prove the intermediate claim H23eq: two_thirds = add_SNo 1 (minus_SNo one_third).
An exact proof term for the current goal is two_thirds_eq_1_minus_one_third.
rewrite the current goal using H23eq (from left to right).
We prove the intermediate claim Hm13R: minus_SNo one_third ∈ R.
An exact proof term for the current goal is (real_minus_SNo one_third H13R).
We prove the intermediate claim Hm13S: SNo (minus_SNo one_third).
An exact proof term for the current goal is (SNo_minus_SNo one_third H13S).
rewrite the current goal using (mul_SNo_distrL c 1 (minus_SNo one_third) HcS SNo_1 Hm13S) (from left to right).
rewrite the current goal using (mul_SNo_oneR c HcS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_minus_distrR c one_third HcS H13S) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HyloS0: SNo (add_SNo (minus_SNo 1) c).
An exact proof term for the current goal is (SNo_add_SNo (minus_SNo 1) c Hm1S HcS).
We prove the intermediate claim HcmulS: SNo (add_SNo c (minus_SNo (mul_SNo c one_third))).
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo c one_third)) HcS Hm_c13S).
rewrite the current goal using (add_SNo_assoc (minus_SNo 1) c (minus_SNo (mul_SNo c one_third)) Hm1S HcS Hm_c13S) (from right to left) at position 1.
rewrite the current goal using HcmulEq (from right to left).
Use reflexivity.
We prove the intermediate claim HlowRle: Rle (add_SNo (minus_SNo 1) (mul_SNo c two_thirds)) (add_SNo y z).
rewrite the current goal using Hylo_zlo_eq (from right to left) at position 1.
An exact proof term for the current goal is Hylzlo2.
Set yhi to be the term add_SNo 1 (minus_SNo c).
Set zhi to be the term mul_SNo c one_third.
We prove the intermediate claim HyhiR: yhi ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo c) HmcR).
We prove the intermediate claim HyhiS: SNo yhi.
An exact proof term for the current goal is (real_SNo yhi HyhiR).
We prove the intermediate claim HzhiR: zhi ∈ R.
An exact proof term for the current goal is Hc13R.
We prove the intermediate claim HzhiS: SNo zhi.
An exact proof term for the current goal is Hc13S.
We prove the intermediate claim Hyzhi: Rle (add_SNo y z) (add_SNo yhi z).
An exact proof term for the current goal is (Rle_add_SNo_1 y yhi z HyR HyhiR HzR HyHi).
We prove the intermediate claim Hupper2: Rle (add_SNo yhi z) (add_SNo yhi zhi).
An exact proof term for the current goal is (Rle_add_SNo_2 yhi z zhi HyhiR HzR HzhiR HzHi).
We prove the intermediate claim Hupper: Rle (add_SNo y z) (add_SNo yhi zhi).
An exact proof term for the current goal is (Rle_tra (add_SNo y z) (add_SNo yhi z) (add_SNo yhi zhi) Hyzhi Hupper2).
We prove the intermediate claim Hyhi_zhi_eq: add_SNo yhi zhi = add_SNo 1 (minus_SNo (mul_SNo c two_thirds)).
We prove the intermediate claim HyhiDef: yhi = add_SNo 1 (minus_SNo c).
Use reflexivity.
We prove the intermediate claim HzhiDef: zhi = mul_SNo c one_third.
Use reflexivity.
rewrite the current goal using HyhiDef (from left to right).
rewrite the current goal using HzhiDef (from left to right).
We prove the intermediate claim HcmulEq: add_SNo c (minus_SNo (mul_SNo c one_third)) = mul_SNo c two_thirds.
We prove the intermediate claim H23eq: two_thirds = add_SNo 1 (minus_SNo one_third).
An exact proof term for the current goal is two_thirds_eq_1_minus_one_third.
rewrite the current goal using H23eq (from left to right).
We prove the intermediate claim Hm13R: minus_SNo one_third ∈ R.
An exact proof term for the current goal is (real_minus_SNo one_third H13R).
We prove the intermediate claim Hm13S: SNo (minus_SNo one_third).
An exact proof term for the current goal is (SNo_minus_SNo one_third H13S).
rewrite the current goal using (mul_SNo_distrL c 1 (minus_SNo one_third) HcS SNo_1 Hm13S) (from left to right).
rewrite the current goal using (mul_SNo_oneR c HcS) (from left to right) at position 1.
rewrite the current goal using (mul_SNo_minus_distrR c one_third HcS H13S) (from left to right) at position 1.
Use reflexivity.
We prove the intermediate claim HcmulNegEq: minus_SNo (mul_SNo c two_thirds) = add_SNo (minus_SNo c) (mul_SNo c one_third).
rewrite the current goal using HcmulEq (from right to left) at position 1.
We prove the intermediate claim HcmulS: SNo (add_SNo c (minus_SNo (mul_SNo c one_third))).
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo c one_third)) HcS Hm_c13S).
We prove the intermediate claim HnegD: minus_SNo (add_SNo c (minus_SNo (mul_SNo c one_third))) = add_SNo (minus_SNo c) (minus_SNo (minus_SNo (mul_SNo c one_third))).
An exact proof term for the current goal is (minus_add_SNo_distr c (minus_SNo (mul_SNo c one_third)) HcS Hm_c13S).
rewrite the current goal using HnegD (from left to right).
rewrite the current goal using (minus_SNo_invol (mul_SNo c one_third) Hc13S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo c) (mul_SNo c one_third) SNo_1 HmcS Hc13S) (from right to left) at position 1.
rewrite the current goal using HcmulNegEq (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim HhiRle: Rle (add_SNo y z) (add_SNo 1 (minus_SNo (mul_SNo c two_thirds))).
rewrite the current goal using Hyhi_zhi_eq (from right to left) at position 1.
An exact proof term for the current goal is Hupper.
An exact proof term for the current goal is (closed_intervalI_of_Rle (add_SNo (minus_SNo 1) (mul_SNo c two_thirds)) (add_SNo 1 (minus_SNo (mul_SNo c two_thirds))) (add_SNo y z) (real_add_SNo (minus_SNo 1) Hm1R (mul_SNo c two_thirds) Hc23R) (real_add_SNo 1 real_1 (minus_SNo (mul_SNo c two_thirds)) (real_minus_SNo (mul_SNo c two_thirds) Hc23R)) HsumR HlowRle HhiRle).
∎