proposition: Lemma SplitR_resp_Qeq : forall (s t:StepF) (a b:OpenUnit), a == b -> StepF_Qeq s t -> StepF_Qeq (SplitR s a) (SplitR t b).
proof: Proof. induction s; induction t; intros a b Hab Hst; simpl in *; try assumption; try contradiction. destruct Hst as [Ho [Hst1 Hst2]]. apply SplitR_glue_ind; intros Hao; apply SplitR_glue_ind; intros Hbo; repeat split; auto with *; try solve [elim (Qlt_not_le _ _ Hao); rewrite -> Hab; rewrite -> Ho; try rewrite -> Hbo; auto with * |elim (Qlt_not_le _ _ Hbo); rewrite <- Hab; rewrite <- Ho; try rewrite -> Hao; auto with *]; try apply IHs1; try apply IHs2; auto with *; simpl; try (rewrite -> Hab; rewrite -> Ho; reflexivity). Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields