proposition: Lemma omd_cb a b l: (1 - (((1 - l) *: # a + l *: # b) *m (# b)^T) 0 0) = (1-l) * omd a b + l * omd b b.
proof: Proof. apply /eqP. rewrite mulmxDl mxE -!scalemxAl ![(_ *: (_ *m (_)^T)) 0 0]mxE opprD. rewrite eq_sym. rewrite /omd/omd_v !mulrBr !mulr1. rewrite !addrA addrAC addrC !addrA [l + 1]addrC. by rewrite -!addrA addrC addrA subrr add0r addrC !addrA 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