proposition: Lemma OTsum_Mle1 a b c d: a <=t b -> c <=t d -> (a+t c) <=t (b+t d).
proof: Proof. move => le1 le2. move: cdo_wor => [wor sr]. pose f := (variantLc a c). pose g := (variantLc b d). have ha: substrate canonical_doubleton_order = domain f by rewrite sr/f; aw. have hb: substrate canonical_doubleton_order = domain g by rewrite sr/g; aw. have hc: (forall x, inc x (domain f) -> Vg f x <=t Vg g x). by rewrite /f /g; aw => i idx; try_lvariant idx. move:(OT_sum_increasing2 (proj1 wor) ha hb hc). by rewrite - OT_sum2_pr - OT_sum2_pr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)