proposition: Lemma apart_negate (x : F) (Px : x ≶ 0) : (-x) ≶ 0.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.apartness HoTT.Classes.theory.rings