proposition: Lemma SplitR_glue_ind : forall s1 s2 (a b:OpenUnit) (P:StepF -> Prop), (forall (H:a < b), P (glue (OpenUnitDualDiv b a H) (SplitR s1 (OpenUnitDiv a b H)) s2)) -> (forall (H:b < a), P (SplitR s2 (OpenUnitDualDiv a b H))) -> (a == b -> P (s2)) -> P (SplitR (glue b s1 s2) a).
proof: Proof. intros. apply (SplitLR_glue_ind s1 s2 a b (fun a b => P b)); assumption. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields