Lemma neghfiberstntonat ( n m : nat ) ( is : natgeh m n ) : ¬ ( hfiber ( stntonat n ) m ). Proof. intros. intro h. destruct h as [ j e ]. destruct j as [ j is' ]. simpl in e. rewrite e in is'. apply ( natgehtonegnatlth _ _ is is' ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.