proposition: Lemma lt_add_eq : forall x1 x2 s1 s1' s2 s2', Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' -> O.eq x1 x2 -> lt s1 s2 -> lt s1' s2'.
proof: Proof. intros x1 x2 s1 s1' s2 s2' Ab1 Ab2 Ad1 Ad2 Hx (x & EQ & Disj). assert (O.lt x1 x). - destruct Disj as [(IN,_)|(IN,_)]; auto. rewrite Hx; auto. - exists x; split. + intros z Hz. rewrite (Ad1 z), (Ad2 z). split; intros [U|U]; try (left; order); right. * rewrite <- (EQ z); auto. * rewrite (EQ z); auto. + destruct Disj as [(IN,Em)|(IN & y & INy & LTy & Be)]. * left; split; auto. -- rewrite (Ad2 x); auto. -- intros z. rewrite (Ad1 z); intros [U|U]; try specialize (Ab1 z U); auto; order. * right; split; auto. -- rewrite (Ad1 x); auto. -- exists y; repeat split; auto. ++ rewrite (Ad2 y); auto. ++ intros z. rewrite (Ad2 z). intros [U|U]; try specialize (Ab2 z U); auto; order. Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts