proposition: Lemma iscoantisymmnatgth (n m : nat) : ¬ (n > m) -> (m > n) ⨿ (n = m).
proof: Proof. revert n m. apply isantisymmnegtoiscoantisymm. - apply isdecrelnatgth. - intros n m. apply isantisymmnegnatgth. Defined.
imports: UniMath.Foundations.Sets