proposition: Theorem lap_add_compat : ∀ α (r : ring α) a b c d, lap_eq a c → lap_eq b d → lap_eq (lap_add a b) (lap_add c d).
proof: Proof. intros α r a b c d Hac Hbd. rewrite Hac, Hbd; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation