proposition: Lemma separateCr (a b c d : Plane) : separate a b c d = separate a b d c.
proof: Proof. rewrite/separate mulrC ![_ _ c d]betweenC; congr andb. by rewrite -Bool.implb_curry andbC Bool.implb_curry andbC. 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)