proposition: Lemma diff_inf : forall (s s' : t) (Hs : Ok s) (Hs' : Ok s') (a : elt), Inf a s -> Inf a s' -> Inf a (diff s s').
proof: Proof. intros s s'; repeat rewrite <- isok_iff; revert s s'. induction2. - apply Hrec; trivial. + apply Inf_lt with x; auto. + apply Inf_lt with x'; auto. - apply Hrec'; auto. apply Inf_lt with x'; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists