proposition: Lemma stronger_transitivity : forall l1 l2 l3, stronger l1 l2 -> stronger l2 l3 -> l2 <> nil -> stronger l1 l3.
proof: Proof. intros l1 l2 l3 Hs1 Hs2 Hl2 x z Hx Hz. destruct l2. intuition. unfold stronger in *. specialize Hs1 with x P. specialize Hs2 with P z. simpl in *. auto. Qed.
imports: List