proposition: Lemma neghfiberstntonat ( n m : nat ) ( is : natgeh m n ) : ¬ ( hfiber ( stntonat n ) m ).
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions