proposition: Lemma part_int_id : Feq I FId (PartInt (IId (Hab:=Hab))).
proof: Proof. apply eq_imp_Feq. red in |- *; simpl in |- *; intros; auto. unfold I in |- *; apply included_refl. intros; simpl in |- *; algebra. Qed.
imports: CoRN.ftc.IntervalFunct