proposition: Theorem Qpositive_le_total : forall w w' : Qpositive, Qpositive_le w w' \/ Qpositive_le w' w.
proof: Proof. intros w w'; cut (Qpositive_le' w w' \/ Qpositive_le' w' w). intros H; elim H; intros H1; generalize (Qpositive_le'_to_Qpositive_le _ _ H1); auto. unfold Qpositive_le' in |- *. case (Qpositive_i w'); case (Qpositive_i w); intros p q p' q'. elim (Nat.le_gt_cases (p * q') (p' * q)); auto with arith. Qed.