proposition: Lemma reverse_involutive p : reverse (reverse p) = p.
proof: Proof. induction p as [p IH|p IH|]; simpl. - by rewrite reverse_xI, reverse_app, IH. - by rewrite reverse_xO, reverse_app, IH. - reflexivity. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)