proposition: Lemma lte_le_dadd a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
proof: Proof. rewrite !dual_addeE lteN2 -lteN2; exact: lte_le_sub. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed