proposition: Lemma is_left_oriented (p q r : Plane) : encompass.is_left (@wccw R) p q r = wccw p q r.
proof: Proof. apply/idP/idP; last by rewrite/encompass.is_left; move=>->; rewrite !orbT. by move=>/or3P[| |//] /eqP re; subst r; rewrite /wccw det_cyclique; [rewrite det_cyclique |]; rewrite det_alternate. 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)