proposition: Theorem mulℝ_proper_realizer : forall e, mulℝ_proper↓e ⊩ ∀x₁ x₂ y₁ y₂, (x₁ ≡ x₂ → y₁ ≡ y₂ → x₁ * y₁ ≡ x₂ * y₂)%Re.
proof: Proof. do 2 Ksolve. startn 7. eapply prop_guard. Kmove. exists ε₁0, ε₁1. Ksolve; now apply Qclt_le_weak. intro Hlex. Kmove. exists ε₂0, ε₂1, q₂0, q₂1; find; (now apply Qclt_le_weak) || apply (prop_subst_stack Hπ). clear_realizers. subst. intro Hley. destruct (Qclt_le_dec ε₁0 ε₁1); destruct (Qclt_le_dec ε₂0 ε₂1). + replace (q₁0 * q₂0 - q₁1 * q₂1) with (q₁0 * (q₂0 - q₂1) + (q₁0 - q₁1) * q₂1) by ring. transitivity (0 + ε₂). - rewrite Qcplus_0_l. etransitivity. now apply Qcabs_triangle. etransitivity; [| eok]. do 2 rewrite Qcabs_mult. apply Qcplus_le_compat. * apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite Qcle_minus_iff. replace (|q₁1| + (ε₁1 + ε₁1) + - |q₁0|) with (ε₁1 + ε₁1 + - (|q₁0| - |q₁1|)) by ring. rewrite <- Qcle_minus_iff. etransitivity. apply Qcabs_triangle_reverse. etransitivity. eok. apply Qcplus_le_compat. now apply Qclt_le_weak. reflexivity. etransitivity. eok. apply Qcplus_le_compat. now apply Qclt_le_weak. reflexivity. * rewrite Qcmult_comm. apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. reflexivity. revert Hc6. Qcunfold. lra. etransitivity. eok. apply Qcplus_le_compat. now apply Qclt_le_weak. reflexivity. - apply Qcplus_le_compat; ok || reflexivity. + replace (q₁0 * q₂0 - q₁1 * q₂1) with (q₁0 * (q₂0 - q₂1) + (q₁0 - q₁1) * q₂1) by ring. etransitivity. apply Qcabs_triangle. do 2 rewrite Qcabs_mult. apply Qcplus_le_compat. - etransitivity; [| eok]. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. * apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. reflexivity. revert Hc1. Qcunfold. lra. etransitivity. eok. apply Qcplus_le_compat. reflexivity. assumption. * apply Qcmult_resp_nonneg. change 0 with (0 + 0). apply Qcplus_le_compat. now apply Qcabs_nonneg. revert Hc2. Qcunfold. lra. revert Hc1. Qcunfold. lra. - etransitivity; [| eok]. rewrite <- Qcplus_0_l at 1. apply Qcplus_le_compat. * apply Qcmult_resp_nonneg. change 0 with (0 + 0). apply Qcplus_le_compat. now apply Qcabs_nonneg. revert Hc5. Qcunfold. lra. revert Hc6. Qcunfold. lra. * rewrite Qcmult_comm. apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. reflexivity. revert Hc6. Qcunfold. lra. etransitivity. eok. apply Qcplus_le_compat. now apply Qclt_le_weak. reflexivity. + rewrite Qcabs_minus. replace (q₁1 * q₂1 - q₁0 * q₂0) with (q₁1 * (q₂1 - q₂0) + (q₁1 - q₁0) * q₂0) by ring. etransitivity. apply Qcabs_triangle. do 2 rewrite Qcabs_mult. rewrite Qcplus_comm. apply Qcplus_le_compat. - etransitivity; [| eok]. rewrite <- Qcplus_0_l at 1. apply Qcplus_le_compat. * apply Qcmult_resp_nonneg. change 0 with (0 + 0). apply Qcplus_le_compat. now apply Qcabs_nonneg. revert Hc1. Qcunfold. lra. revert Hc2. Qcunfold. lra. * rewrite Qcmult_comm. apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. reflexivity. revert Hc2. Qcunfold. lra. etransitivity. rewrite Qcabs_minus. eok. apply Qcplus_le_compat. reflexivity. assumption. - etransitivity; [| eok]. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. * apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. reflexivity. revert Hc5. Qcunfold. lra. etransitivity. rewrite Qcabs_minus. eok. apply Qcplus_le_compat. now apply Qclt_le_weak. reflexivity. * apply Qcmult_resp_nonneg. change 0 with (0 + 0). apply Qcplus_le_compat. now apply Qcabs_nonneg. revert Hc6. Qcunfold. lra. revert Hc5. Qcunfold. lra. + rewrite Qcabs_minus. replace (q₁1 * q₂1 - q₁0 * q₂0) with (q₁1 * (q₂1 - q₂0) + (q₁1 - q₁0) * q₂0) by ring. transitivity (ε₁ + 0). - rewrite Qcplus_0_r. etransitivity. now apply Qcabs_triangle. etransitivity; [| eok]. do 2 rewrite Qcabs_mult. apply Qcplus_le_compat. * apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite Qcle_minus_iff. replace (|q₁0| + (ε₁0 + ε₁0) + - |q₁1|) with (ε₁0 + ε₁0 + - (|q₁1| - |q₁0|)) by ring. rewrite <- Qcle_minus_iff. etransitivity. apply Qcabs_triangle_reverse. etransitivity. rewrite Qcabs_minus. eok. apply Qcplus_le_compat. reflexivity. assumption. etransitivity. rewrite Qcabs_minus. eok. apply Qcplus_le_compat. reflexivity. assumption. * rewrite Qcmult_comm. apply Qcmult_le_compat. now apply Qcabs_nonneg. now apply Qcabs_nonneg. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. reflexivity. revert Hc2. Qcunfold. lra. etransitivity. rewrite Qcabs_minus. eok. apply Qcplus_le_compat. reflexivity. assumption. - apply Qcplus_le_compat; ok || reflexivity. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations