proposition: Lemma lee_dadd2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b).
proof: Proof. by move=> ?; rewrite !dual_addeE leeN2 leeD2lE ?fin_numN// leeN2. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed