Theorem edist_vadd_vadd_le

Modification history