proposition: Lemma Separated_Refinement_lft : Refinement P Separated_Refinement.
proof: Proof. exists RSR_auxP; repeat split. exact RSR_auxP_lemman. intros; apply RSR_auxP_lemma1; assumption. exact RSR_auxP_lemma2. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)