proposition: Theorem multpf_dist_plusl : forall (p q r : list (Term A n)) (a : Term A n), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> eqP A eqA n (multpf p (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec q r)) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (multpf p q) (multpf p r)).
proof: Proof. Proof using os minusA invA divA cs A1. intros p q r H' H'0 H'1 H'2. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multpf (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec q r) p); auto. apply multpf_com; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (multpf q p) (multpf r p)); auto. apply multpf_dist_plusr; auto. apply eqp_pluspf_com with (1 := cs); auto. apply multpf_com; auto. apply multpf_com; auto. Qed.