{ g : forall (y : No), { x_plus_y : No & (forall l, (xL_plus l).1 y < x_plus_y) * (forall r, x_plus_y < (xR_plus r).1 y) } & (forall y z : No, y <= z -> (g y).1 <= (g z).1) * (forall y z : No, y < z -> (g y).1 < (g z).1) }. Proof. simple refine (No_ind_package (fun y => { x_plus_y : No & (forall l, (xL_plus l).1 y < x_plus_y) * (forall r, x_plus_y < (xR_plus r).1 y) }) (fun _ _ _ z w => z.1 <= w.1) (fun _ _ _ z w => z.1 < w.1) _ _ _ _ _). - intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR. pose (L'' := L + L'). pose (R'' := R + R'). pose (zL := sum_ind (fun _ => No) (fun l => (xL_plus l).1 {{ yL | yR // ycut }}) (fun l => (x_plus_yL l).1) : L'' -> No). pose (zR := sum_ind (fun _ => No) (fun r => (xR_plus r).1 {{ yL | yR // ycut }}) (fun r => (x_plus_yR r).1) : R'' -> No). assert (zcut : forall (l:L'') (r:R''), zL l < zR r). { abstract ( intros [l|l] [r|r]; cbn; [ apply xL_lt_xR_plus | transitivity ((xL_plus l).1 (yR r)); [ apply (snd (xL_plus l).2), lt_ropt; exact _ | exact (fst (x_plus_yR r).2 l) ] | transitivity ((xR_plus r).1 (yL l)); [ exact (snd (x_plus_yL l).2 r) | apply (snd (xR_plus r).2), lt_lopt; exact _ ] | apply x_plus_yL_lt_yR ]). } assert (InSort S L'' R'') by (apply sum_options; exact _). exists ({{ zL | zR // zcut }}); split. + intros l. refine (lt_lopt zL zR zcut (inl l)). + intros r. refine (lt_ropt zL zR zcut (inl r)). - abstract ( intros x y [a ?] [b ?] p q r s; rewrite transport_sigma; cbn in *; apply path_sigma_hprop, path_No; cbn; rewrite transport_const; assumption). - abstract ( intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR L'' R'' ? zL zR zcut x_plus_zL x_plus_zR x_plus_zL_lt_zR yL_lt_z x_plus_yL_lt_z y_lt_zR x_plus_y_lt_zR; cbn in *; apply le_lr; [ intros [l|l] | intros [r|r] ]; cbn; [ refine (le_lt_trans (fst (xL_plus l).2 _ {{ zL | zR // zcut}} _) _); [ by (apply le_lr; assumption) | refine (lt_lopt _ _ _ (inl l)) ] | exact (x_plus_yL_lt_z l) | refine (lt_le_trans _ (fst (xR_plus r).2 {{ yL | yR // ycut}} _ _)); [ refine (lt_ropt _ _ _ (inl r)) | by (apply le_lr; assumption) ] | exact (x_plus_y_lt_zR r) ] ). - abstract ( intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR L'' R'' ? zL zR zcut x_plus_zL x_plus_zR x_plus_zL_lt_zR l y_le_zL x_plus_y_le_zL; cbn; apply lt_l with (inr l); apply x_plus_y_le_zL ). - abstract ( intros L' R' ? yL yR ycut x_plus_yL x_plus_yR x_plus_yL_lt_yR L'' R'' ? zL zR zcut x_plus_zL x_plus_zR x_plus_zL_lt_zR r yR_le_z x_plus_yR_le_z; cbn; apply lt_r with (inr r); apply x_plus_yR_le_z). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.