proposition: Theorem lap_eq_sym {α} {r : ring α} : symmetric _ lap_eq.
proof: Proof. intros l₁ l₂ Heq. revert l₂ Heq. induction l₁ as [| x₁]; intros. induction l₂ as [| x₂]; constructor; apply lap_eq_nil_cons_inv in Heq. destruct Heq; assumption. apply IHl₂; destruct Heq; assumption. induction l₂ as [| x₂]. apply lap_eq_cons_nil_inv in Heq; destruct Heq. constructor; [ assumption | apply IHl₁; assumption ]. apply lap_eq_cons_inv in Heq; destruct Heq. constructor; [ symmetry; assumption | apply IHl₁; assumption ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation