Assume Hcneg: c < 0.

Set d to be the term minus_SNo c.

We prove the intermediate claim HdR: d ∈ R.

An exact proof term for the current goal is (real_minus_SNo c HcR).

We prove the intermediate claim HdS: SNo d.

An exact proof term for the current goal is (real_SNo d HdR).

We prove the intermediate claim Hdpos: 0 < d.

rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.

An exact proof term for the current goal is (minus_SNo_Lt_contra c 0 HcS SNo_0 Hcneg).

We prove the intermediate claim Hcontd: continuous_map R R_standard_topology R R_standard_topology (mul_const_fun d).

An exact proof term for the current goal is (mul_const_fun_continuous_pos d HdR Hdpos).

We prove the intermediate claim Hnegcont: continuous_map R R_standard_topology R R_standard_topology neg_fun.

An exact proof term for the current goal is neg_fun_continuous.

We prove the intermediate claim Hcomp: continuous_map R R_standard_topology R R_standard_topology (compose_fun R (mul_const_fun d) neg_fun).

An exact proof term for the current goal is (composition_continuous R R_standard_topology R R_standard_topology R R_standard_topology (mul_const_fun d) neg_fun Hcontd Hnegcont).

We prove the intermediate claim Heq: compose_fun R (mul_const_fun d) neg_fun = mul_const_fun c.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ compose_fun R (mul_const_fun d) neg_fun.

We will prove z ∈ mul_const_fun c.

Apply (ReplE_impred R (λt0 : set ⇒ (t0,apply_fun neg_fun (apply_fun (mul_const_fun d) t0))) z Hz (z ∈ mul_const_fun c)) to the current goal.

Let t be given.

Assume HtR: t ∈ R.

Assume HzEq: z = (t,apply_fun neg_fun (apply_fun (mul_const_fun d) t)).

rewrite the current goal using HzEq (from left to right).

We prove the intermediate claim Hdef: mul_const_fun c = graph R (λt0 : set ⇒ mul_SNo t0 c).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

We prove the intermediate claim HtS: SNo t.

An exact proof term for the current goal is (real_SNo t HtR).

We prove the intermediate claim HmulR: mul_SNo t d ∈ R.

An exact proof term for the current goal is (real_mul_SNo t HtR d HdR).

We prove the intermediate claim Hrhs: apply_fun neg_fun (apply_fun (mul_const_fun d) t) = mul_SNo t c.

rewrite the current goal using (mul_const_fun_apply d t HdR HtR) (from left to right) at position 1.

rewrite the current goal using (neg_fun_apply (mul_SNo t d) HmulR) (from left to right) at position 1.

We prove the intermediate claim Hcd: c = minus_SNo d.

We prove the intermediate claim HdDef: d = minus_SNo c.

Use reflexivity.

rewrite the current goal using HdDef (from left to right).

rewrite the current goal using (minus_SNo_minus_SNo_R c HcR) (from left to right).

Use reflexivity.

rewrite the current goal using Hcd (from left to right) at position 2.

We prove the intermediate claim Htmp: mul_SNo t (minus_SNo d) = minus_SNo (mul_SNo t d).

An exact proof term for the current goal is (mul_SNo_minus_distrR t d HtS HdS).

rewrite the current goal using Htmp (from left to right).

Use reflexivity.

We prove the intermediate claim HpairEq: (t,apply_fun neg_fun (apply_fun (mul_const_fun d) t)) = (t,mul_SNo t c).

rewrite the current goal using Hrhs (from left to right).

Use reflexivity.

rewrite the current goal using HpairEq (from left to right).

An exact proof term for the current goal is (ReplI R (λt0 : set ⇒ (t0,mul_SNo t0 c)) t HtR).

Let z be given.

Assume Hz: z ∈ mul_const_fun c.

We will prove z ∈ compose_fun R (mul_const_fun d) neg_fun.

We prove the intermediate claim Hdef: mul_const_fun c = graph R (λt0 : set ⇒ mul_SNo t0 c).

Use reflexivity.

We prove the intermediate claim HzGraph: z ∈ graph R (λt0 : set ⇒ mul_SNo t0 c).

rewrite the current goal using Hdef (from right to left).

An exact proof term for the current goal is Hz.

Apply (ReplE_impred R (λt0 : set ⇒ (t0,mul_SNo t0 c)) z HzGraph (z ∈ compose_fun R (mul_const_fun d) neg_fun)) to the current goal.

Let t be given.

Assume HtR: t ∈ R.

Assume HzEq: z = (t,mul_SNo t c).

rewrite the current goal using HzEq (from left to right).

We prove the intermediate claim HdefComp: compose_fun R (mul_const_fun d) neg_fun = {(t0,apply_fun neg_fun (apply_fun (mul_const_fun d) t0))|t0 ∈ R}.

Use reflexivity.

rewrite the current goal using HdefComp (from left to right).

We prove the intermediate claim HtS: SNo t.

An exact proof term for the current goal is (real_SNo t HtR).

We prove the intermediate claim HmulR: mul_SNo t d ∈ R.

An exact proof term for the current goal is (real_mul_SNo t HtR d HdR).

We prove the intermediate claim Hlhs: apply_fun neg_fun (apply_fun (mul_const_fun d) t) = mul_SNo t c.

rewrite the current goal using (mul_const_fun_apply d t HdR HtR) (from left to right) at position 1.

rewrite the current goal using (neg_fun_apply (mul_SNo t d) HmulR) (from left to right) at position 1.

We prove the intermediate claim Hcd: c = minus_SNo d.

We prove the intermediate claim HdDef: d = minus_SNo c.

Use reflexivity.

rewrite the current goal using HdDef (from left to right).

rewrite the current goal using (minus_SNo_minus_SNo_R c HcR) (from left to right).

Use reflexivity.

rewrite the current goal using Hcd (from left to right) at position 2.

We prove the intermediate claim Htmp: mul_SNo t (minus_SNo d) = minus_SNo (mul_SNo t d).

An exact proof term for the current goal is (mul_SNo_minus_distrR t d HtS HdS).

rewrite the current goal using Htmp (from left to right).

Use reflexivity.

rewrite the current goal using Hlhs (from right to left).

Apply (ReplI R (λt0 : set ⇒ (t0,apply_fun neg_fun (apply_fun (mul_const_fun d) t0))) t HtR) to the current goal.

rewrite the current goal using Heq (from right to left).

An exact proof term for the current goal is Hcomp.

Assume Hc0: c = 0.

rewrite the current goal using Hc0 (from left to right).

We prove the intermediate claim HmEq: mul_const_fun 0 = const_fun R 0.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ mul_const_fun 0.

We will prove z ∈ const_fun R 0.

Apply (ReplE_impred R (λt0 : set ⇒ (t0,mul_SNo t0 0)) z Hz (z ∈ const_fun R 0)) to the current goal.

Let t be given.

Assume HtR: t ∈ R.

Assume HzEq: z = (t,mul_SNo t 0).

rewrite the current goal using HzEq (from left to right).

We prove the intermediate claim HtS: SNo t.

An exact proof term for the current goal is (real_SNo t HtR).

rewrite the current goal using (mul_SNo_zeroR t HtS) (from left to right).

An exact proof term for the current goal is (ReplI R (λt0 : set ⇒ (t0,0)) t HtR).

Let z be given.

Assume Hz: z ∈ const_fun R 0.

We will prove z ∈ mul_const_fun 0.

Apply (ReplE_impred R (λt0 : set ⇒ (t0,0)) z Hz (z ∈ mul_const_fun 0)) to the current goal.

Let t be given.

Assume HtR: t ∈ R.

Assume HzEq: z = (t,0).

rewrite the current goal using HzEq (from left to right).

We prove the intermediate claim HtS: SNo t.

An exact proof term for the current goal is (real_SNo t HtR).

We prove the intermediate claim HpairEq: (t,0) = (t,mul_SNo t 0).

rewrite the current goal using (mul_SNo_zeroR t HtS) (from left to right) at position 1.

Use reflexivity.

rewrite the current goal using HpairEq (from left to right).

An exact proof term for the current goal is (ReplI R (λt0 : set ⇒ (t0,mul_SNo t0 0)) t HtR).

rewrite the current goal using HmEq (from left to right).

An exact proof term for the current goal is (const_fun_continuous R R_standard_topology R R_standard_topology 0 R_standard_topology_is_topology_local R_standard_topology_is_topology_local real_0).