proposition: Lemma direct_uniq p q r : ccw p q r -> uniq [:: p; q; r].
proof: Proof. move=>pqr. apply/andP; split. 2: by rewrite in_cons 2!in_nil orbF 2!andbT; apply/eqP; apply (@direct_distincts q r p); rewrite /ccw 2!det_cyclique. rewrite negb_or orbF; apply/andP; split. by apply/eqP; exact (direct_distincts pqr). by rewrite eq_sym; apply/eqP; apply (@direct_distincts r p q); rewrite /ccw det_cyclique. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)