proposition: Lemma is_left_oriented (p q r : Plane) : encompass.is_left oriented p q r = oriented 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 /oriented det_cyclique; [ rewrite det_cyclique |]; rewrite det_alternate. Qed.
imports: encompass conv mathcomp(all_ssreflect all_algebra vector reals normedtype) mathcomp(classical_sets boolp mathcomp_extra) counterclockwise mathcomp.algebra_tactics(ring) mathcomp.zify(zify)