proposition: Lemma field_split2 (x : F) : (x * recip' 2 (positive_apart_zero 2 lt_0_2)) + (x * recip' 2 (positive_apart_zero 2 lt_0_2)) = x.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.fields HoTT.Classes.orders.rings