Definition isantisymmnatleh : isantisymm natleh. Proof. intros m. induction m as [|m M]. - intros n _ s. unfold natleh in s. apply pathsinv0. apply nat1gthtois0. exact s. - intros n. induction n as [|n _]. + intros r _. contradicts r (negnatlehsn0 m). + intros r s. change (S m ≤ S n) with (m ≤ n) in r. change (S n ≤ S m) with (n ≤ m) in s. apply (maponpaths S). apply M. * assumption. * assumption. Defined.