proposition: Lemma pihomog_is_linear : linear pihomog.
proof: Proof. move=> c p q /=; pose_big_enough l. rewrite (pihomogwE _ (k := l)) //. rewrite (pihomogwE _ (k := l) (p := p)) //. rewrite (pihomogwE _ (k := l) (p := q)) //. rewrite scaler_sumr -big_split /=; apply: eq_bigr => m _. by rewrite linearP /= scalerDl scalerA. by close. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg