proposition: Theorem mults_ltP_comp : forall (a : Term A n) (p q : list (Term A n)), ltP (A:=A) (n:=n) ltM p q -> ltP (A:=A) (n:=n) ltM (mults a p) (mults a q).
proof: Proof. Proof using os. intros a p q H'; elim H'; simpl in |- *; auto. intros x y p0 q0 H'0; simpl in |- *; apply ltP_hd; auto. apply multTerm_ltT_l with (1 := os); auto. Qed.