proposition: Lemma SplitLSplitL : forall (s:StepF) (a b c:OpenUnit), (a*b==c) -> (StepF_Qeq (SplitL (SplitL s a) b) (SplitL s c)).
proof: Proof. induction s. intros a b c _. apply StepF_Qeq_refl. intros a b c H. apply SplitL_glue_ind; intros Hao. apply SplitL_glue_ind; intros Hco. apply IHs1. simpl. rewrite <- H; field. auto with *. elim (Qlt_not_le a c). apply Qlt_trans with o; assumption. rewrite <- H. replace RHS with (1*a). replace LHS with (b*a). apply Qmult_le_compat_r; auto with *. now simpl; ring. now simpl; ring. elim (Qlt_not_le a c). rewrite -> Hco. apply Qlt_le_trans with o; auto with *. rewrite <- H. replace RHS with (1*a). replace LHS with (b*a). apply Qmult_le_compat_r; auto with *. now simpl; ring. now simpl; ring. apply SplitL_glue_ind; intros Hbd. apply SplitL_glue_ind; intros Hco. apply SplitL_resp_Qeq; auto with *. simpl. rewrite <- H. field; auto with *. elim (Qlt_not_le _ _ Hbd). simpl. apply Qle_shift_div_r; auto with *. rewrite -> Qmult_comm; rewrite -> H; auto with *. elim (Qlt_not_le _ _ Hbd). simpl. apply Qle_shift_div_r; auto with *. rewrite -> Qmult_comm; rewrite -> H; rewrite -> Hco; auto with *. apply SplitL_glue_ind; intros Hco. elim (Qlt_not_le _ _ Hbd). simpl. apply Qle_shift_div_l; auto with *. rewrite -> Qmult_comm; rewrite -> H; auto with *. repeat split; auto with *. simpl. rewrite <- H. field; auto with *. apply IHs2. simpl. rewrite <- H. field; repeat split; auto with *. clear - Hao; rewrite -> Qlt_minus_iff in Hao. auto with *. elim (Qlt_not_le _ _ Hbd). simpl. apply Qle_shift_div_l; auto with *. rewrite -> Qmult_comm; rewrite -> H; auto with *. assert (Y:o==c). rewrite <- H. rewrite -> Hbd. simpl. field. auto with *. apply SplitL_glue_ind; intros Hco; try (elim (Qlt_not_le _ _ Hco); rewrite -> Y; auto with * ). auto with *. apply SplitL_glue_ind; intros Hco. apply SplitL_resp_Qeq; auto with *. simpl. rewrite <- H. rewrite -> Hao. field; auto with *. elim (Qlt_not_le _ _ Hco). rewrite <- H. rewrite <- Hao. replace RHS with (1*a). replace LHS with (b*a). apply Qmult_le_compat_r; auto with *. now simpl; ring. now simpl; ring. elim (Qlt_not_le b 1). auto with *. rewrite <- Hao in Hco. rewrite -> Hco in H. apply Qmult_lt_0_le_reg_r with a. auto with *. ring_simplify. rewrite -> H. auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields