(x : F) (Px : x ≶ 0) : (-x) ≶ 0. Proof. assert (ap : x + 0 ≶ x - x). { rewrite (plus_0_r x). rewrite (plus_negate_r x). assumption. } refine (Trunc_rec _ (field_plus_ext F x 0 x (-x) ap)). intros [apxx|ap0x]. - destruct (apart_ne x x apxx); reflexivity. - symmetry; assumption. Qed.
Require Import