proposition: Theorem lap_add_comm : ∀ al₁ al₂, lap_eq (lap_add al₁ al₂) (lap_add al₂ al₁).
proof: Proof. intros al₁ al₂. revert al₂. induction al₁; intros. destruct al₂; [ apply lap_eq_refl | simpl ]. constructor; [ reflexivity | apply lap_eq_refl ]. destruct al₂. constructor; [ reflexivity | apply lap_eq_refl ]. constructor; [ apply rng_add_comm | apply IHal₁ ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation