proposition: Lemma included_refl' : forall a b Hab Hab', included (compact a b Hab) (compact a b Hab').
proof: Proof. intros. red in |- *; intros x H. inversion_clear H; split; auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists