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