proposition: Theorem lap_add_opp_l : ∀ α (r : ring α) la, (- la + la = 0)%lap.
proof: Proof. intros α r la. induction la as [| a]; [ reflexivity | simpl ]. rewrite IHla, rng_add_opp_l. constructor; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation