proposition: Lemma stronger2__stronger_right : forall l1 l2 l2', stronger l1 l2 -> stronger l1 l2' -> stronger l1 (l2++l2').
proof: Proof. intros l1 l2 l2' Hs Hs' x y Hx Hy. apply in_app_or in Hy. destruct Hy. apply Hs; assumption. apply Hs'; assumption. Qed.
imports: List