proposition: Lemma lte_pdaddl y x z : 0 <= x -> y < z -> y < x + z.
proof: Proof. by move=> x0 /lt_le_trans; apply; rewrite lee_pdaddl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed