proposition: Lemma dup_app p q : dup (p ++ q) = dup p ++ dup q.
proof: Proof. revert p. induction q as [p IH|p IH|]; intros q; simpl. - by rewrite IH. - by rewrite IH. - reflexivity. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)