fact: Definition separate (a b c d : Plane) := (det a b c * det a b d <= 0) && ((a == b) ==> between a c d) && ((det a b c == 0) ==> (det a b d == 0) ==> (a != b) ==> [|| between a c d, between b c d | (between c a b && between d a b)]).
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)