Lemma notboth {r s} : (r<s) -> ¬ (s<r). Proof. intros l m. simple refine (pr1 (strongly_from_weakly_well_founded wwf_lt (λ t, ¬ ((r=t) ⨿ (s=t))) _) r (ii1 (idpath r))). intros x h c. induction c as [e|e]. + induction e. exact (h s m (ii2 (idpath s))). + induction e. exact (h r l (ii1 (idpath r))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.