proposition: Lemma swapB (p q : Plane) : swap (p-q) = swap p - swap q.
proof: Proof. by rewrite swapD swapN. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)