proposition: Lemma od_bound a: forall n, a < double n -> snd (od a) < n.
proof: Proof. induction a using nat_ind_2; intros n Hn; simpl. destruct n; simpl. discriminate. reflexivity. destruct n; simpl. discriminate. reflexivity. revert IHa. case od; simpl. intros o a' IH. destruct n. discriminate. apply IH, Hn. Qed.
imports: List PeanoNat common comparisons