proposition: Lemma separateCl (a b c d : Plane) : separate a b c d = separate b a c d.
proof: Proof. rewrite/separate 2![det _ b _]det_inverse mulrN mulNr opprK. rewrite -2![det a _ _]det_cyclique 2!oppr_eq0 eq_sym. rewrite orbA (orbC (_ a c d)) -orbA. congr (_ && _ && (_ ==> _ ==> _ ==> (_ || _))). - by apply implyb_id2l=>/eqP->. - by rewrite !(@betweenC _ _ a b). 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)