proposition: Lemma omd_cc a b l: 1 - (((1 - l) *: # a + l *: # b) *m ((1 - l) *: # a + l *: # b)^T) 0 0 = (1-l)^+2 * omd a a + l^+2 * omd b b + l * (1-l) * omd a b *+2.
proof: Proof. apply /eqP. rewrite mulmxDl mxE -!scalemxAl ![(_ *: (_ *m (_)^T)) 0 0]mxE opprD. rewrite ![#_*m_^T]dotC addrA. have: 1 == (l*1+(1-l)*1) by rewrite !mulr1 addrCA subrr addr0. move=> /eqP l_eq. rewrite {1}l_eq -[l*1 + _ + _]addrA -mulrBr addrAC -mulrBr. rewrite omd_ca omd_cb mulrDr mulrDr. rewrite addrACA [X in X + _]addrC mulrA -expr2. rewrite addrA addrAC [(1 - l) * (l * omd a b)]mulrCA. rewrite -[X in X +_ == _]addrA addrAC mulrA -expr2. by rewrite !addrA !mulrA eqxx. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence