{ f : No -> { g : No -> No & (forall x y, x <= y -> g x <= g y) * (forall x y, x < y -> g x < g y) } & (forall x y, x <= y -> forall z, (f x).1 z <= (f y).1 z) * (forall x y, x < y -> forall z, (f x).1 z < (f y).1 z) }. Proof. refine (No_rec_package {g : No -> No & (forall x y, x <= y -> g x <= g y) * (forall x y, x < y -> g x < g y) } (fun g h => forall x, g.1 x <= h.1 x) (fun g h => forall x, g.1 x < h.1 x) (fun L R Sx xL xR xcut xL_plus xR_plus xL_lt_xR_plus => let g := plus_inner xL_plus xR_plus xL_lt_xR_plus in ((fun y => (g.1 y).1) ; (g.2))) _ _ _ _). - abstract ( intros [g ?] [h ?] p q; apply path_sigma_hprop; cbn in *; apply path_arrow; intros x; apply path_No; [ apply p | apply q ] ). - abstract ( intros L R ? xL xR xcut xL_plus xR_plus xL_lt_xR_plus L' R' ? yL yR ycut yL_plus yR_plus yL_lt_yR_plus; intros xL_lt_y xL_lt_y_plus x_lt_yR x_lt_yR_plus z; lazy beta zeta in *; cbn [pr1] in *; pattern z; refine (No_ind_hprop _ _ z); intros L'' R'' ? zL zR zcut x_le_y_plus_zL x_le_y_plus_zR; destruct (plus_inner_cut xL_plus xR_plus xL_lt_xR_plus zL zR zcut) as [xzcut p]; rewrite p; destruct (plus_inner_cut yL_plus yR_plus yL_lt_yR_plus zL zR zcut) as [yzcut q];rewrite q; apply le_lr; [ intros [l|l] | intros [r|r] ]; [ specialize (xL_lt_y_plus l {{ zL | zR // zcut }}); rewrite q in xL_lt_y_plus; exact xL_lt_y_plus | refine (le_lt_trans (x_le_y_plus_zL l) _); refine (lt_lopt _ _ _ (inr l)) | specialize (x_lt_yR_plus r {{ zL | zR // zcut }}); rewrite p in x_lt_yR_plus; exact x_lt_yR_plus | refine (lt_le_trans _ (x_le_y_plus_zR r)); refine (lt_ropt _ _ _ (inr r)) ]). - abstract ( intros L R ? xL xR xcut xL_plus xR_plus xL_lt_xR_plus L' R' ? yL yR ycut yL_plus yR_plus yL_lt_yR_plus; intros l x_le_yL x_le_yL_plus z; lazy beta zeta in *; cbn [pr1] in *; pattern z; refine (No_ind_hprop _ _ z); intros L'' R'' ? zL zR zcut x_le_y_plus_zL x_le_y_plus_zR; destruct (plus_inner_cut xL_plus xR_plus xL_lt_xR_plus zL zR zcut) as [xzcut p]; rewrite p; destruct (plus_inner_cut yL_plus yR_plus yL_lt_yR_plus zL zR zcut) as [yzcut q];rewrite q; refine (le_lt_trans (x_le_yL_plus {{ zL | zR // zcut }}) _); refine (lt_lopt _ _ _ (inl l)) ). - abstract ( intros L R ? xL xR xcut xL_plus xR_plus xL_lt_xR_plus L' R' ? yL yR ycut yL_plus yR_plus yL_lt_yR_plus; intros r xR_le_y xR_le_y_plus z; lazy beta zeta in *; cbn [pr1] in *; pattern z; refine (No_ind_hprop _ _ z); intros L'' R'' ? zL zR zcut x_le_y_plus_zL x_le_y_plus_zR; destruct (plus_inner_cut xL_plus xR_plus xL_lt_xR_plus zL zR zcut) as [xzcut p]; rewrite p; destruct (plus_inner_cut yL_plus yR_plus yL_lt_yR_plus zL zR zcut) as [yzcut q];rewrite q; refine (lt_le_trans _ (xR_le_y_plus {{ zL | zR // zcut }})); refine (lt_ropt _ _ _ (inl r)) ). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.