proposition: Lemma MirrorSplitL_Qeq : forall (s:StepF) (a b:OpenUnit), b == (OpenUnitDual a) -> (StepF_Qeq (Mirror (SplitL s a)) (SplitR (Mirror s) b)).
proof: Proof. induction s. auto with *. intros a b Hab; simpl in Hab. simpl. apply SplitL_glue_ind; intros Hao; apply: SplitR_glue_ind; intros Hoa; simpl in Hoa; try (repeat split; auto with *; try apply IHs1; try apply IHs2; simpl; rewrite -> Hab; field; auto with * ). elim (Qlt_not_le _ _ Hao). rewrite -> Qlt_minus_iff in Hoa. rewrite -> Qle_minus_iff. replace RHS with (1 - o + - (1 - a)). rewrite <- Hab. auto with *. now simpl; ring. elim (Qlt_not_le _ _ Hao). rewrite -> Qle_minus_iff. replace RHS with (1 - o + - (1 - a)). rewrite <- Hab. rewrite <- Hoa. ring_simplify. auto with *. now simpl; ring. intros H; ring_simplify in H. revert H; change (~(a==0)); auto with *. elim (Qlt_not_le _ _ Hao). rewrite -> Qle_minus_iff. rewrite -> Qlt_minus_iff in Hoa. replace RHS with (1 - a + - (1 - o)). rewrite <- Hab. auto with *. now simpl; ring. elim (Qlt_not_le _ _ Hao). rewrite -> Qle_minus_iff. replace RHS with (1 - a + - (1 - o)). rewrite <- Hab. rewrite <- Hoa. ring_simplify. auto with *. now simpl; ring. elim (Qlt_not_le _ _ Hoa). rewrite -> Hab. rewrite -> Hao. auto with *. elim (Qlt_not_le _ _ Hoa). rewrite -> Hab. rewrite -> Hao. auto with *. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields