proposition: Lemma addN x : x - x == 0.
proof: Proof. apply eqR_sym; split=> [c [a ltxa [b lt_ac_b /leRq-lebx]] | d d_gt0]. by rewrite ltcE -(ltr_addr (- a)) ltr_oppl (lt_trans lt_ac_b) ?lebx. have [[a ltxa] [b lebx]] := (cut_ub x, cut_lb x). have{a ltxa d_gt0} []: exists n, x < b + d *+ n. have ltab: (0 < a - b)%R by move/leRq in lebx; rewrite subr_gt0 lebx. pose c := ((a - b) / d)%R; have c_ge0: (0 <= c)%R by rewrite ltW ?divr_gt0. exists `|numq c|%N; apply: ltc_le_trans ltxa _; rewrite -ler_subl_addl. rewrite pmulrn gez0_abs -?ge_rat0 // -mulrzl numqE mulrAC. by rewrite divfK ?gt_eqF ?ler_pmulr // ler1z -gtz0_ge1 denq_gt0. elim=> [|n IHn]; rewrite ?addr0 // mulrSr => /open[a ltxa lt_a_dnd]. have [/IHn//| le_bdn_x] := classical (x < b + d *+ n). by exists a => //; exists (b + d *+ n)%R; rewrite // opprB ltr_subl_addr -addrA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)