proposition: Lemma reverse_go_app p1 p2 p3 : reverse_go p1 (p2 ++ p3) = reverse_go p1 p3 ++ reverse_go 1 p2.
proof: Proof. revert p3 p1 p2. cut (∀ p1 p2 p3, reverse_go (p2 ++ p3) p1 = p2 ++ reverse_go p3 p1). { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. } intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto. - apply (IH _ (_~1)). - apply (IH _ (_~0)). Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)