proposition: Lemma poly_diff_z_eq : forall {n} {b1} (p1 : poly b1 n) {b2} (p2 : poly b2 n), (plus p1 (poly_neg p2)).1 = true -> (_ ; p1) = (_; p2) :> { null : bool & poly null n }.
proof: Proof. intros. depind p1; depelim p2; auto; try (autorewrite with poly_neg plus in H; discriminate; fail). - destruct z; destruct i; autorewrite with poly_neg plus in *; discriminate. - f_equal; destruct z as [ | z | z], z0 as [ | z0 | z0 ]; depelim i; depelim i0; autorewrite with poly_neg plus in H. assert (z = z0). remember (Z.pos z + Z.neg z0)%Z as z1; destruct z1; try discriminate; simpl in H; nia. subst; auto. remember (Z.pos z + Z.pos z0)%Z as z1; destruct z1; try discriminate. remember (Z.neg z + Z.neg z0)%Z as z1; destruct z1; try discriminate. assert (z = z0). remember (Z.neg z + Z.pos z0)%Z as z1; destruct z1; try discriminate; simpl in H; nia. subst; auto. - autorewrite with poly_neg plus in H. specialize (IHp1 _ p2 H). depelim IHp1. auto. - autorewrite with poly_neg plus in H. specialize (IHp1_1 _ p2_1); specialize (IHp1_2 _ p2_2). remember (plus p1_2 (poly_neg p2_2)) as P; remember (plus p1_1 (poly_neg p2_1)) as Q. destruct P as [bP P]; destruct Q as [bQ Q]. destruct bP; destruct bQ; simpl in H; try rewrite <- HeqQ in H; try discriminate. specialize (IHp1_1 eq_refl); specialize (IHp1_2 eq_refl). depelim IHp1_1; try depelim IHp1_2; auto. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef