proposition: Theorem ps_lap_in_compat : ∀ α (R : ring α) (K : field R) a b la lb, (a = b)%ps → (la = lb)%pslap → ps_lap_in a la → ps_lap_in b lb.
proof: Proof. intros α R K a b la lb Hab Hlab Hla. unfold ps_lap_eq in Hlab. revert a b Hab lb Hlab Hla. induction la as [| c]; intros; [ contradiction | idtac ]. simpl in Hla. destruct Hla as [(Hcla, Hca)| Hla]. destruct lb as [| d]; [ contradiction | idtac ]. apply lap_eq_cons_inv in Hlab. destruct Hlab as (Hcd, Hlab). left. split. intros H; apply Hcla; clear Hcla. rewrite <- H. constructor; assumption. rewrite <- Hcd, <- Hab; assumption. simpl. destruct lb as [| d]. apply lap_eq_cons_nil_inv in Hlab. destruct Hlab as (Hc, Hlab). eapply IHla; eassumption. apply lap_eq_cons_inv in Hlab. destruct Hlab as (Hcd, Hlab). right. eapply IHla; eassumption. Qed.
imports: Utf8 QArith NPeano Sorted Misc NbarM QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHull ConvexHullMisc PolyConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq