proposition: Lemma strict_sub_trans2 : forall a b c : E, sub a b -> strict_sub b c -> strict_sub a c.
proof: Proof. unfold strict_sub in |- *. unfold neq in |- *. unfold not in |- *. ir. xd. ir. ap H0. ap extensionality. am. rewrite <- H2. am. xd. apply sub_trans with b; au. Qed.
imports: tactics