(x : F) : (x * recip' 2 (positive_apart_zero 2 lt_0_2)) + (x * recip' 2 (positive_apart_zero 2 lt_0_2)) = x. Proof. rewrite <- plus_mult_distr_l. rewrite <- (mult_1_l (recip' 2 (positive_apart_zero 2 lt_0_2))). rewrite <- plus_mult_distr_r. rewrite (recip_inverse' 2 (positive_apart_zero 2 lt_0_2)). rewrite mult_1_r. reflexivity. Qed.
Require Import