proposition: Lemma RS'_delta_pos : [0][<]delta.
proof: Proof. unfold delta in |- *; apply less_Min. assumption. apply div_resp_pos. apply mult_resp_pos. astepl (nring (R:=IR) 0); apply nring_less; apply RS'_pos_n. apply pos_max_one. assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)