proposition: Lemma RS_delta_csi : delta[<=]csi.
proof: Proof. unfold delta in |- *; eapply leEq_transitive. apply Min_leEq_rht. eapply leEq_transitive. apply Min_leEq_rht. apply Min_leEq_lft. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions