Lemma chaintrans {x y z m n} : chain lt m x y -> chain lt n y z -> chain lt (m+n) x z. Proof. revert m n y. apply (diagRecursion (λ m n, ∏ y, chain lt m x y → chain lt n y z → chain lt (m + n) x z)). - intros k y c. induction c. exact (idfun _). - intros r s p y c d. induction c as [u [t [b [k e]]]]. change ((S r) + s) with (S (r+s)). rewrite plus_n_Sm. apply (p u b); clear p b x r. induction e. exact (cons1 lt z (idpath u) k d). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.