(x : No) : x + negate x = zero. Proof. unfold No in *; repeat_No_ind_hprop; destruct (negate_cut xL xR xcut) as [nxcut p]; rewrite p; clear p; do_plus_cut. apply path_No. - apply le_lr; [ intros [l|r]; cbn [sum_ind] | intros [] ]. + unfold zero in IHL; rewrite <- (IHL l); clear IHL. apply plus_lt_r. refine (lt_ropt _ _ _ l). + unfold zero in IHR; rewrite <- (IHR r); clear IHR. apply plus_lt_l. refine (lt_ropt _ _ _ r). - apply le_lr; [ intros [] | intros [r|l] ]; cbn [sum_ind]. + unfold zero in IHR; rewrite <- (IHR r); clear IHR. apply plus_lt_r. refine (lt_lopt _ _ _ r). + unfold zero in IHL; rewrite <- (IHL l); clear IHL. apply plus_lt_l. refine (lt_lopt _ _ _ l). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.