Definition iscoantisymmnatlth (n m : nat) : ¬ (natlth n m) -> (natlth m n) ⨿ (n = m). Proof. intros nlnm. induction (iscoantisymmnatgth m n nlnm) as [ l | e ]. - apply (ii1 l). - apply (ii2 (pathsinv0 e)). Defined.