proposition: Theorem get_coef_eq {n} b1 b2 (p1 : poly b1 n) (p2 : poly b2 n) : (forall (m : mono n), get_coef m p1 = get_coef m p2) -> (b1 ; p1) = (b2 ; p2) :> { null : _ & poly null n}.
proof: Proof. Proof with (simp get_coef in *; auto). intros Hcoef. induction p1 as [ | z Hz | n b p1 | n b p1 IHp q1 IHq ] in b2, p2, Hcoef |- *; [dependent elimination p2 as [poly_z | poly_c z i] | dependent elimination p2 as [poly_z | poly_c z' i'] | dependent elimination p2 as [@poly_l n b' p2 | @poly_s n b' p2 q2] ..]. all:(intros; try rename n0 into n; auto; try (specialize (Hcoef mono_z); simp get_coef in Hcoef; subst z; (elim i || elim Hz || ltac:(repeat f_equal; auto)); fail)). - specialize (IHp1 _ p2). forward IHp1. intro m. specialize (Hcoef (mono_l m))... clear Hcoef. dependent elimination IHp1 as [eq_refl]. reflexivity. - destruct (poly_nz q2) as [m HNZ]. specialize (Hcoef (mono_s m))... rewrite <- Hcoef in HNZ; elim HNZ. - destruct (poly_nz q1) as [m HNZ]. specialize (Hcoef (mono_s m))... rewrite Hcoef in HNZ; elim HNZ. - forward (IHq _ q2). intro m. specialize (Hcoef (mono_s m))... apply f_equal. forward (IHp _ p2). intro. specialize (Hcoef (mono_l m))... depelim IHp. now depelim IHq. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef