Lemma isantisymmnegnatgth (n m : nat) : ¬ (n > m) -> ¬ (m > n) -> n = m. Proof. revert m. induction n as [ | n IHn ]. - intros m ng0m ngm0. apply (pathsinv0 (negnatgth0tois0 _ ngm0)). - intro m. destruct m as [ | m ]. + intros ngsn0 ng0sn. induction (ngsn0 (natgthsn0 _)). + intros ng1 ng2. apply (maponpaths S (IHn m ng1 ng2)). Defined.