proposition: Lemma intersectCl (a b c d : Plane) : intersect a b c d = intersect b a c d.
proof: Proof. by rewrite/intersect separateCl; congr andb; apply separateCr. Qed.
imports: counterclockwise conv encompass preliminaries mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets constructive_ereal) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)