proposition: Lemma Separated_Refinement_rht : Refinement R Separated_Refinement.
proof: Proof. exists RSR_auxR; repeat split. exact RSR_auxR_lemmam. intros; apply RSR_auxR_lemma1; assumption. exact RSR_auxR_lemma2. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)