proposition: Theorem div_rr : forall x1 x2 y1 y2 : R, forall xi yi zi : FF, REL x1 x2 xi -> REL y1 y2 yi -> NZR y2 -> div_rr_helper xi yi zi = true -> REL (x1 / y1) (x2 / y2) zi.
proof: Proof. intros x1 x2 y1 y2 xi yi zi (xe,(Hx1,Hx2)) (ye,(Hy1,Hy2)) Hy4 Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H4). generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). apply Fle2_m1_correct in H1. apply Flt2_m1_correct in H2. generalize (Fle2_correct _ _ H3). repeat rewrite Fplus2_correct. rewrite Fmult2_correct. clear H3. intro H3. generalize (Fle2_correct _ _ H4). repeat rewrite Fplus2_correct. rewrite Fmult2_correct. clear H4. intro H4. exists ((xe - ye) / (1 + ye))%R. split. apply IRcompose_inv with (1 := H1) (2 := H2) (3 := H4) (4 := H3) (5 := Hx1) (6 := Hy1). rewrite Hx2. rewrite Hy2. field. split. apply Rgt_not_eq. apply Rlt_le_trans with (2 := Rplus_le_compat_l R1 _ _ (proj1 Hy1)). rewrite <- (Rplus_opp_r 1). apply Rplus_lt_compat_l with (1 := H2). exact Hy4. Qed.
imports: Gappa_common Gappa_pred_bnd