proposition: Lemma RS_Hd' : forall x y : IR, I x -> I y -> forall Hx Hy, AbsIR (x[-]y)[<=]d -> AbsIR (F x Hx[-]F y Hy)[<=]e.
proof: Proof. unfold d in |- *; elim (contF' e RS_He); auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions