proposition: Theorem lap_eq_trans {α} {r : ring α} : transitive _ lap_eq.
proof: Proof. intros l₁ l₂ l₃ H₁ H₂. revert l₁ l₃ H₁ H₂. induction l₂ as [| x₂]; intros. revert l₃ H₂. induction l₁ as [| x₁]; intros; [ assumption | idtac ]. destruct l₃ as [| x₃]; [ assumption | idtac ]. apply lap_eq_cons_nil_inv in H₁. apply lap_eq_nil_cons_inv in H₂. constructor. etransitivity; [ destruct H₁; eassumption | idtac ]. destruct H₂; symmetry; assumption. apply IHl₁; [ destruct H₁ | destruct H₂ ]; assumption. destruct l₁ as [| x₁]. apply lap_eq_nil_cons_inv in H₁. destruct l₃ as [| x₃]; constructor. apply lap_eq_cons_inv in H₂. destruct H₁, H₂. etransitivity; [ symmetry; eassumption | assumption ]. apply lap_eq_cons_inv in H₂. apply IHl₂; [ destruct H₁ | destruct H₂ ]; assumption. apply lap_eq_cons_inv in H₁. destruct l₃ as [| x₃]; constructor. apply lap_eq_cons_nil_inv in H₂. destruct H₁, H₂. etransitivity; eassumption. apply lap_eq_cons_nil_inv in H₂. apply IHl₂; [ destruct H₁ | destruct H₂ ]; assumption. apply lap_eq_cons_inv in H₂. destruct H₁, H₂. etransitivity; eassumption. apply lap_eq_cons_inv in H₂. apply IHl₂; [ destruct H₁ | destruct H₂ ]; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation