proposition: Theorem lap_compose_compat : ∀ la lb lc ld, lap_eq la lc → lap_eq lb ld → lap_eq (lap_compose la lb) (lap_compose lc ld).
proof: Proof. intros la lb lc ld Hac Hbd. rewrite Hac, Hbd; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation