proposition: Lemma SplitRSplitR : forall (s:StepF) (a b c:OpenUnit), (a+b-a*b==c) -> (StepF_Qeq (SplitR (SplitR s a) b) (SplitR s c)).
proof: Proof. intros s a b c H. apply StepF_Qeq_trans with (Mirror (Mirror (SplitR (SplitR s a) b))); auto with *. apply StepF_Qeq_trans with (Mirror (Mirror (SplitR s c))); auto with *. apply Mirror_resp_Qeq. apply StepF_Qeq_trans with (SplitL (SplitL (Mirror s) (OpenUnitDual a)) (OpenUnitDual b)). apply StepF_Qeq_trans with (SplitL (Mirror (SplitR s a)) (OpenUnitDual b)). apply MirrorSplitR_Qeq; auto with *. apply SplitL_resp_Qeq; auto with *. apply MirrorSplitR_Qeq; auto with *. apply StepF_Qeq_trans with (SplitL (Mirror s) (OpenUnitDual c)). apply SplitLSplitL. simpl. rewrite <- H. ring. apply StepF_Qeq_sym. apply MirrorSplitR_Qeq; auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields