proposition: Lemma strict_sub_nonempty_complement : forall x y : E, strict_sub x y -> nonempty (complement y x).
proof: Proof. ir. assert (nonemptyT (complement y x)). ap not_empty_nonemptyT. uhg; ir. uh H; ee. ap H. ap extensionality. am. uhg; ir. ap excluded_middle. uhg; ir. assert (inc x0 (complement y x)). rw inc_complement. xd. uh H0. ufi not H0. apply H0 with x0. am. nin H0. cp (R_inc X0). sh (R X0). am. Qed.
imports: Arith order