proposition: Theorem poly_add_assoc : ∀ pol₁ pol₂ pol₃, (pol₁ + (pol₂ + pol₃) = (pol₁ + pol₂) + pol₃)%pol.
proof: Proof. intros pol₁ pol₂ pol₃. unfold eq_poly. eapply lap_add_assoc; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation