proposition: Lemma Rplus_le_lt_reg_r : forall a b c d, b + a <= c + a < d + a -> b <= c < d.
proof: Proof. intros a b c d H. split. now apply Rplus_le_reg_r with a. now apply Rplus_lt_reg_r with a. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core) Gappa(Gappa_tactic)