fact: Definition le (a b:A) : Prop := match a with | inl a' => match b with | inl b' => O1.le a' b' | _ => True end | inr a' => match b with | inr b' => O2.le a' b' | _ => False end end.
imports: Relations List ZArith