proposition: Lemma lt_add_lt : forall x1 x2 s1 s1' s2 s2', Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' -> O.lt x1 x2 -> lt s1' s2'.
proof: Proof. intros x1 x2 s1 s1' s2 s2' Ab1 Ab2 Ad1 Ad2 LT. exists x1; split; [ | right; split]; auto. - intros y Hy. rewrite (Ad1 y), (Ad2 y). split; intros [U|U]; try order. + specialize (Ab1 y U). order. + specialize (Ab2 y U). order. - rewrite (Ad1 x1); auto with *. - exists x2; repeat split; auto. + rewrite (Ad2 x2); now left. + intros y. rewrite (Ad2 y). intros [U|U]. * order. * specialize (Ab2 y U). order. Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts