proposition: Lemma RS_delta_pos : [0][<]delta.
proof: Proof. unfold delta in |- *; apply less_Min; apply less_Min. unfold deltaP in |- *; apply pos_AntiMesh; [ apply RS_pos_n | assumption ]. unfold deltaR in |- *; apply pos_AntiMesh; [ apply RS_pos_m | assumption ]. apply div_resp_pos. apply pos_max_one. apply pos_div_two; assumption. apply less_Min. assumption. apply RS_Hd. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions