proposition: Lemma f_char : forall a b, f a b == (a+b)/(1-a*b).
proof: Proof. intros [x y] [w z]. unfold f. rewrite -> Qred_correct. destruct (Z.eq_dec (y*z) (x*w)) as [H|H]. unfold Qmult. simpl ((Qnum (x # y) * Qnum (w # z) # Qden (x # y) * Qden (w # z))). repeat rewrite <- H. replace (y * z - y * z)%Z with 0%Z by ring. setoid_replace (1-(y * z # y * z)) with 0. change ((x * z + y * w)%Z * 0 == ((x # y) + (w # z)) * 0). ring. rewrite -> (Qmake_Qdiv (y*z)). change (1 - (y * z)%positive / (y * z)%positive == 0). field; discriminate. unfold Zminus. repeat rewrite -> injz_plus. change (((x * Zpos z) + (Zpos y * w)) / (Zpos y * Zpos z - x * w) == ((x # y) + (w # z)) / (1 - (x #y)*(w # z))). repeat rewrite -> Qmake_Qdiv. field. repeat split; try discriminate. cut (~(y * z)%Z == (x * w)%Z). intros X Y. apply X. replace RHS with ((x * w)%Z + 0) by simpl; ring. rewrite <- Y. change ((y * z) == (x * w) + (y * z - x * w)). ring. intros X; apply H. unfold Qeq in X. simpl in X. rewrite Pmult_1_r in X. change ((y * z)%Z = (x * w * 1)%Z) in X. rewrite X. ring. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.Q_in_CReals CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRarctan_small CoRN.transc.MoreArcTan CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q