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