fact: Definition scalar_product (p q: Plane) := p.1 * q.1 + p.2 * q.2.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)