proposition: Lemma orient2d_spec : forall x1 y1 x2 y2 x3 y3, generic_format radix2 fxp x1 -> generic_format radix2 fxp y1 -> generic_format radix2 fxp x2 -> generic_format radix2 fxp y2 -> generic_format radix2 fxp x3 -> generic_format radix2 fxp y3 -> let M := (norm2d (x1 - x3) (x2 - x3) * norm2d (y1 - y3) (y2 - y3))%R in hombnd' M M (orient2d x1 y1 x2 y2 x3 y3) (orient2d_exact x1 y1 x2 y2 x3 y3) (Float radix2 5846006549323612646370400306145384485685829828610 (-212)) (Float radix2 2 0).
proof: Proof. intros x1 y1 x2 y2 x3 y3 Fx1 Fy1 Fx2 Fy2 Fx3 Fy3. assert (Sx13 := hombnd_sub_init x1 x3 Fx1 Fx3). assert (Sy13 := hombnd_sub_init y1 y3 Fy1 Fy3). assert (Sx23 := hombnd_sub_init x2 x3 Fx2 Fx3). assert (Sy23 := hombnd_sub_init y2 y3 Fy2 Fy3). apply (hombnd_fact' (Rmax_l _ (Rabs (x2 - x3)))) in Sx13. apply (hombnd_fact' (Rmax_l _ (Rabs (y2 - y3)))) in Sy13. apply (hombnd_fact' (Rmax_r (Rabs (x1 - x3)) _)) in Sx23. apply (hombnd_fact' (Rmax_r (Rabs (y1 - y3)) _)) in Sy23. assert (M1 := hombnd_mul Sx13 Sy23). assert (M2 := hombnd_mul Sx23 Sy13). clear Sx13 Sy23 Sx23 Sy13. apply hombnd_rnd'' in M1. apply hombnd_rnd'' in M2. assert (D := hombnd_sub M1 M2). clear M1 M2. apply hombnd_rnd' in D. rewrite Rmin_left in D by apply Rle_refl. exact D. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)