proposition: Lemma ler_addl_abs : forall x₁ x₂, x₁ <<= x₂ -> forall y, (absr y) <<= (x₂ - x₁) -> x₁ <<= x₂ + y .
proof: Proof. move=> x1 x2 hx12 y; move/le_absr. rewrite -(@lerTlb x2) addrC oppr_add opprK. by rewrite addrA addrN add0r addrC. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)