proposition: Lemma gte_dopp (r : \bar^d R) : (0 < r)%E -> (- r < r)%E.
proof: Proof. by case: r => //= r; rewrite !lte_fin; apply: gtrN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed