fact: Definition invert_Some {A} (x : option A) : match x with | Some _ => A | None => unit end := match x with | Some x' => x' | None => tt end.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround