proposition: Lemma SplitLSplitR : forall (s:StepF) (a b c d:OpenUnit), (a+b-a*b==c) -> (d*c==a) -> (StepF_Qeq (SplitL (SplitR s a) b) (SplitR (SplitL s c) d)).
proof: Proof. induction s. intros a b c d _ _. apply StepF_Qeq_refl. intros a b c d H0 H1. apply SplitR_glue_ind; intros Hao. assert (Hao':~ o - a == 0). intros H. elim (Qlt_not_le _ _ Hao). rewrite -> Qle_minus_iff. replace RHS with (- (o- a)). rewrite -> H. auto with *. now simpl; ring. apply SplitL_glue_ind; intros Hbz; simpl in Hbz. apply SplitL_glue_ind; intros Hco. apply IHs1; simpl; [rewrite <- H0|rewrite <- H1]; field; auto with *. elim (Qlt_not_le _ _ Hbz). rewrite -> Qlt_minus_iff in Hco. rewrite -> Qle_minus_iff. replace RHS with ((a + b - a*b + -o)/(1 -a)). rewrite -> H0. apply Qle_shift_div_l; auto with *. replace LHS with 0. auto with *. now simpl; ring. now (simpl; field; auto with * ). elim (Qlt_not_le _ _ Hbz). rewrite -> Qle_minus_iff. replace RHS with ((a + b - a*b + -o)/(1 -a)). rewrite -> H0. rewrite -> Hco. replace RHS with 0. auto with *. now (simpl; field; auto with * ). now (simpl; field; auto with * ). apply SplitL_glue_ind; intros Hco. elim (Qlt_not_le _ _ Hbz). rewrite -> Qlt_minus_iff in Hco. rewrite -> Qle_minus_iff. replace RHS with ((o + -(a + b - a*b))/(1 -a)). rewrite -> H0. apply Qle_shift_div_l; auto with *. replace LHS with 0. auto with *. now simpl; ring. simpl; field. now auto with *. apply SplitR_glue_ind; intros Hdz; simpl in Hdz. repeat split; simpl. field_simplify; auto with *. apply Qmult_comp. rewrite <- H1; ring. apply Qinv_comp. replace LHS with (a + b - a*b - a). rewrite -> H0. replace RHS with (c - (d*c)). rewrite -> H1. reflexivity. now simpl; ring. now simpl; ring. apply SplitR_resp_Qeq; auto with *; simpl. rewrite <- H1; field; auto with *. apply SplitL_resp_Qeq; auto with *; simpl. rewrite <- H0; field; auto with *. elim (Qlt_not_le _ _ Hdz). apply Qle_shift_div_l; auto with *. rewrite -> H1; auto with *. elim (Qlt_not_le _ _ Hao). rewrite <- H1. rewrite -> Hdz. replace RHS with (o:Q). auto with *. simpl. field. now auto with *. elim (Qlt_not_le _ _ Hbz). rewrite <- Hco. rewrite <- H0. replace RHS with (b:Q); [ | simpl; field]; auto with *. apply SplitL_glue_ind; intros Hco. elim (Qlt_not_le _ _ Hco). rewrite <- H0. rewrite -> Hbz. replace RHS with (o:Q); [ | simpl; field]; auto with *. elim (Qlt_not_le _ _ Hco). rewrite <- H0. rewrite -> Hbz. replace LHS with (o:Q); [ | simpl; field]; auto with *. apply SplitR_resp_Qeq; simpl; auto with *. rewrite <- H1. rewrite -> Hco. field; auto with *. apply SplitL_glue_ind; intros Hco. elim (Qlt_not_le _ _ Hco). rewrite <- H0. apply Qlt_le_weak. rewrite -> Qlt_minus_iff in *. replace RHS with (a + - o + b*(1-a)). assert (Z:0 < (1-a)) by auto with *. Qauto_pos. now simpl; ring. assert (Hco':~ c - o == 0). intros H. elim (Qlt_not_le _ _ Hco). rewrite -> Qle_minus_iff. replace RHS with (c-o). rewrite -> H. auto with *. replace LHS with (-(c-o)). rewrite -> H. simpl; ring. now simpl; ring. apply SplitR_glue_ind; intros Hdz; simpl in Hdz. elim (Qlt_not_le _ _ Hdz). apply Qle_shift_div_r; auto with *. rewrite -> H1; auto with *. apply IHs2; simpl; [rewrite <- H0|rewrite <- H1]; field; auto with *. elim (Qlt_not_le _ _ Hao). rewrite <- H1. rewrite -> Hdz. replace LHS with (o:Q); [ | simpl; field]; auto with *. elim (Qlt_not_le _ _ Hao). rewrite <- H1. rewrite <- Hco. rewrite -> Qle_minus_iff. replace RHS with (c * (1-d)). apply Qlt_le_weak. assert (Z:0 < (1-d)) by auto with *. Qauto_pos. now simpl; ring. apply SplitL_glue_ind; intros Hco. elim (Qlt_not_le _ _ Hco). rewrite <- Hao. rewrite <- H1. rewrite -> Qle_minus_iff. replace RHS with (c * (1-d)). apply Qlt_le_weak. assert (Z:0 < (1-d)) by auto with *. Qauto_pos. now simpl; ring. apply SplitR_glue_ind; intros Hdz; simpl in Hdz. elim (Qlt_not_le _ _ Hdz). apply Qle_shift_div_r; auto with *. rewrite <- Hao. rewrite -> H1; auto with *. elim (Qlt_not_le _ _ Hdz). apply Qle_shift_div_l; auto with *. rewrite <- Hao. rewrite -> H1; auto with *. apply SplitL_resp_Qeq; simpl; auto with *. rewrite <- H0. rewrite <- Hao. field; auto with *. elim (Qlt_not_le (d*c) a). rewrite -> Hao. rewrite -> Hco. rewrite -> Qlt_minus_iff. replace RHS with (o * (1-d)). assert (Z:0 < (1-d)) by auto with *. Qauto_pos. now simpl; ring. rewrite -> H1. auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields