Theorem dnihfsq ( n : nat ) ( i : ⟦S n⟧ ) : hfsqstr ( di i ) ( stntonat ( S n ) ) ( stntonat n ) ( dni i ). Proof. intros. apply ( ishfsqweqhfibersgtof' ( di i ) ( stntonat ( S n ) ) ( stntonat n ) ( dni i ) ( dnicommsq _ _ ) ). intro x. destruct ( natlthorgeh x n ) as [ g | l ]. - assert ( is1 : iscontr ( hfiber ( stntonat n ) x ) ). { apply iscontrhfiberstntonat. assumption. } assert ( is2 : iscontr ( hfiber ( stntonat ( S n ) ) ( di i x ) ) ). { apply iscontrhfiberstntonat. apply ( natlehlthtrans _ ( S x ) ( S n ) ( natlehdinsn i x ) g ). } apply isweqcontrcontr. + assumption. + assumption. - assert ( is1 : ¬ ( hfiber ( stntonat ( S n ) ) ( di i x ) ) ). { apply neghfiberstntonat. unfold di. destruct ( natlthorgeh x i ) as [ l'' | g' ]. + destruct ( natgehchoice2 _ _ l ) as [ g' | e ]. * apply g'. * rewrite e in l''. assert ( int := natlthtolehsn _ _ l'' ). contradicts (natgthnegleh (pr2 i)) int. + apply l. } apply ( isweqtoempty2 _ is1 ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.