Lemma stn_ord_inj {n : nat} (f : incl (⟦n⟧) (⟦n⟧)) : (∏ (i j: ⟦n⟧ ), i ≤ j → f i ≤ f j) -> ∏ i, f i = i. Proof. intros inc ?. induction n as [|n I]. - apply fromempty. apply negstn0. assumption. - assert (strincr : is_stn_strictly_increasing (pr1incl _ _ f)). { apply is_incr_impl_strincr. { use (isinclcomp f (stntonat_incl _)). } { exact inc. } } assert (M : stntonat _ (f lastelement) = n). { apply isantisymmnatgeh. * assert (N : f lastelement ≥ f firstelement + n). { exact (stn_ord_incl (pr1incl _ _ f) strincr). } use (istransnatgeh _ _ _ N). apply natgehplusnmm. * exact (stnlt (f lastelement)). } assert (L : ∏ j, f (dni lastelement j) < n). { intros. induction M. apply strincr. apply dni_last_lt. } pose (f'' := inclcomp (inclcomp (make_incl _ (isincldni n lastelement)) f) (make_incl _ (isinclstntonat _))). pose (f' := λ j : ⟦n⟧, make_stn n (f'' j) (L j)). assert (J : isincl f'). { unfold f'. intros x j j'. apply iscontraprop1. * apply isaset_hfiber; apply isasetstn. * use subtypePath. ** intro. apply isasetstn. ** induction j as [j e]. induction j' as [j' e']. simpl. apply (invmaponpathsincl f'' (pr2 f'')). apply (base_paths _ _ (e @ !e')). } assert (F : ∏ j : ⟦n⟧, f' j = j). { apply (I (make_incl _ J)). intros j j' lt. apply inc. change (pr1 (dni lastelement j) ≤ pr1 (dni lastelement j')). rewrite 2?dni_last. assumption. } apply subtypePath_prop. change (stntonat _ (f i) = i). induction (natgehchoice _ _ (lastelement_ge i)) as [ge | eq]. + pose (p := maponpaths (stntonat _) (F (make_stn n i ge))). simpl in p. induction p. change (stntonat _ (f i) = f (dni lastelement (make_stn n i ge))). apply maponpaths, maponpaths, pathsinv0. apply subtypePath_prop. apply dni_last. + apply subtypePath_prop in eq. rewrite <- eq. apply M. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.