proposition: Lemma lteD a b x y : a < b -> x < y -> a + x < b + y.
proof: Proof. move: a b x y=> [a| |] [b| |] [x| |] [y| |]; rewrite ?(ltry,ltNyr)//. by rewrite !lte_fin; exact: ltrD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed