proposition: Lemma affine_transf : forall oy dy y1 y2 y : R, (0 < dy)%R -> (oy + dy * y1 <= y <= oy + dy * y2)%R <-> (y1 <= (y - oy) / dy <= y2)%R.
proof: Proof. intros oy dy y1 y2 y Hdy. replace y with (oy + dy * ((y - oy) / dy))%R at 1 2. 2: now field ; apply Rgt_not_eq. split ; intros [H1 H2] ; split. - apply Rmult_le_reg_l with (1 := Hdy). apply Rplus_le_reg_l with (1 := H1). - apply Rmult_le_reg_l with (1 := Hdy). apply Rplus_le_reg_l with (1 := H2). - apply Rplus_le_compat_l. apply Rmult_le_compat_l with (2 := H1). now apply Rlt_le. - apply Rplus_le_compat_l. apply Rmult_le_compat_l with (2 := H2). now apply Rlt_le. Qed.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog