proposition: Theorem Axiom5' (pivot p q r : Plane) : (pivot : R *l R) < p -> (pivot : R *l R) < q -> (pivot : R *l R) < r -> ccw pivot p q -> ccw pivot q r -> ccw pivot p r.
proof: Proof. rewrite /ccw 3!det_scalar_productE/scalar_product/= !mulrN !subr_gt0 -![(pivot : R *l R) < _]subr_gtlex0 {1 2 3}/lt/=/ProdLexiOrder.lt/= !implybE -!ltNge !le_eqVlt ![(_==_)||_]orbC -!Bool.orb_andb_distrib_r=>/orP; case=>p0. move=>/orP; case=>q0. move=>/orP; case=>r0. rewrite -(ltr_pdivr_mull _ _ p0) mulrA -(ltr_pdivl_mulr _ _ q0) [_^-1*_]mulrC -(ltr_pdivr_mull _ _ q0) mulrA -(ltr_pdivl_mulr _ _ r0) [_^-1*_]mulrC -(ltr_pdivr_mull _ _ p0) mulrA -(ltr_pdivl_mulr _ _ r0) [_^-1*_]mulrC=>qlt rlt; exact (lt_trans qlt rlt). move:r0=>/andP[/eqP<- r0]. by rewrite 2!mulr0 pmulr_rgt0// pmulr_rgt0//. move:q0=>/andP[/eqP<- q0]/orP; case. move=>r0 _; rewrite mul0r pmulr_rlt0// =>r0'. by move: (lt_trans r0 r0'); rewrite ltxx. by move=>/andP[/eqP<- _] _; rewrite mul0r mulr0 ltxx. move:p0=>/andP[/eqP<- p0]. rewrite 2!mul0r pmulr_rlt0// pmulr_rlt0// =>/orP; case. by move=>q0 _ q0'; move:(lt_trans q0 q0'); rewrite ltxx. by move=>/andP[/eqP<- q0]; rewrite ltxx. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)