fact: Fixpoint Qpositive_le_bool (w w' : Qpositive) {struct w'} : bool := match w with | One => match w' with | dL y => false | _ => true end | dL y => match w' with | dL y' => Qpositive_le_bool y y' | _ => true end | nR y => match w' with | nR y' => Qpositive_le_bool y y' | _ => false end end.