proposition: Lemma Sorted_reverse {A} (R : relation A) l : Sorted R l → Sorted (flip R) (reverse l).
proof: Proof. induction 1; rewrite ?reverse_nil, ?reverse_cons; auto using Sorted_snoc, HdRel_reverse. Qed.
imports: stdpp(options)