proposition: Lemma gseq_trans : forall d1 d2 d3 (EQL: gseq d1 d2) (EQR: gseq d2 d3), gseq d1 d3.
proof: Proof. pcofix CIH; intros. punfold EQL. punfold EQR. destruct EQL, EQR; eauto. - exfalso. eapply nonzero_not_infzeros, IZ2. eapply zeros_star_mono; eauto. simpl. intros. subst. destruct R; eauto. - exfalso. eapply nonzero_not_infzeros, IZ1. eapply zeros_star_mono; eauto. simpl. intros. subst. destruct R; eauto. - eapply zeros_star_nonzero_uniq in ZS2; eauto using gseq_cons_or_nil_nonzero_l, gseq_cons_or_nil_nonzero_r. subst. pfold. econstructor 2; eauto. destruct R; dependent destruction R0; pclearbot; eauto. Qed.
imports: ZArith List String Paco.paco Program Classical