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 Hdne0: d ≠ 0.

An exact proof term for the current goal is (SNo_pos_ne0 d HdS Hdpos).

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

An exact proof term for the current goal is (div_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 (div_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 (div_const_fun d) neg_fun Hcontd Hnegcont).

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

Apply set_ext to the current goal.

Let z be given.

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

We will prove z ∈ div_const_fun c.

Apply (ReplE_impred R (λt0 : set ⇒ (t0,apply_fun neg_fun (apply_fun (div_const_fun d) t0))) z Hz (z ∈ div_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 (div_const_fun d) t)).

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 HdivR: div_SNo t d ∈ R.

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

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

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

rewrite the current goal using (neg_fun_apply (div_SNo t d) HdivR) (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: div_SNo t (minus_SNo d) = minus_SNo (div_SNo t d).

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

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

Use reflexivity.

We prove the intermediate claim HpairEq: (t,apply_fun neg_fun (apply_fun (div_const_fun d) t)) = (t,div_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).

We prove the intermediate claim Hdefc: div_const_fun c = graph R (λt0 : set ⇒ div_SNo t0 c).

Use reflexivity.

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

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

Let z be given.

Assume Hz: z ∈ div_const_fun c.

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

We prove the intermediate claim Hdefc: div_const_fun c = graph R (λt0 : set ⇒ div_SNo t0 c).

Use reflexivity.

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

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

An exact proof term for the current goal is Hz.

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

Let t be given.

Assume HtR: t ∈ R.

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

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

We prove the intermediate claim HdefComp: compose_fun R (div_const_fun d) neg_fun = {(t0,apply_fun neg_fun (apply_fun (div_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 HdivR: div_SNo t d ∈ R.

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

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

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

rewrite the current goal using (neg_fun_apply (div_SNo t d) HdivR) (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: div_SNo t (minus_SNo d) = minus_SNo (div_SNo t d).

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

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

Use reflexivity.

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

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

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

An exact proof term for the current goal is Hcomp.