They both use numDomainType as a base field, both have their distance/norm taking values in this field, and the following lemmas ensures that the axioms for metric spaces holds.
normr_ge0 : forall [R : numDomainType] [V : semiNormedZmodType R] (v : V), 0 <= `|v|
normr0P : forall {R : numDomainType} {V : normedZmodType R} {v : V}, reflect (`|v| = 0) (v == 0)
ler_distrD : forall [R : numDomainType] [V : semiNormedZmodType R] (u v w : V), `|v - w| <= `|v - u| + `|u - w|
distrC : forall [R : numDomainType] [V : semiNormedZmodType R] (v w : V), `|v - w| = `|w - v|
They both use numDomainType as a base field, both have their distance/norm taking values in this field, and the following lemmas ensures that the axioms for metric spaces holds.
normr_ge0 : forall [R : numDomainType] [V : semiNormedZmodType R] (v : V), 0 <= `|v| normr0P : forall {R : numDomainType} {V : normedZmodType R} {v : V}, reflect (`|v| = 0) (v == 0) ler_distrD : forall [R : numDomainType] [V : semiNormedZmodType R] (u v w : V), `|v - w| <= `|v - u| + `|u - w| distrC : forall [R : numDomainType] [V : semiNormedZmodType R] (v w : V), `|v - w| = `|w - v|