proposition: Lemma Pmax_le_l (x y: positive): (x <= Pmax x y)%positive.
proof: Proof. Admitted. Lemma Pmax_le_r (x y: positive): (x <= Pmax y x)%positive. Admitted. Hint Immediate Pmax_le_l Pmax_le_r. Program Fixpoint enum' (n: nat): list (sig (ge n)) := match n with | O => nil | S n' => n' :: map (λ x: sig (ge n'), x) (enum' n') end. Lemma enum_enum' (n: nat): enum n = map (@proj1_sig _ _) (enum' n). Proof. induction n; simpl. reflexivity. rewrite IHn, map_map. reflexivity. Qed.
imports: Unicode.Utf8 Program CRArith CRabs Qminmax Qauto Qround Qmetric stdlib_omissions.P stdlib_omissions.Z stdlib_omissions.Q stdlib_omissions.N metric2.Classified util.Container Ranges decision