(* N_ordering.v, 30 Sep 2013 -- 4 Oct 2013 Basic ordering properties of the natural numbers *) Load N_arithmetic. Definition is_nonzero (a : N) : Prop. Proof. induction a. exact False. exact True. Defined. Lemma zero_initial (a : N) : succ a = zero -> False. Proof. intro H. change (is_nonzero zero). rewrite <- H. simpl. trivial. Qed. Lemma zero_decomp (a b : N) : a + b = zero -> a = zero. Proof. induction a. simpl. intro H. reflexivity. intro K. absurd (succ (a + b) = zero). unfold not. apply (zero_initial (a + b)). rewrite <- add_succ_l. apply K. Qed. Definition less (a b:N) : Prop := N_rect (fun _=>Prop) False (fun Pb tv => tv \/ a = Pb) b. Notation "a < b" := (less a b). Lemma less_succ (a : N) : a < succ a. Proof. simpl. tauto. Defined. Lemma less_transitive (a b c : N) : a < b -> b < c -> a < c. Proof. induction c. simpl. tauto. simpl. intro H. left. destruct H0. apply IHc. apply H. exact H0. rewrite <- H0. exact H. Defined. Lemma less_succ_cancel (a b : N) : succ a < succ b -> a < b. Proof. simpl. intro H. destruct H. assert (a < succ a). simpl. right. reflexivity. apply (less_transitive a (succ a) b). exact H0. exact H. rewrite <- H. apply less_succ. Defined. Lemma less_irreflexive (a : N) : a < a -> False. Proof. simpl. induction a. tauto. intro H. apply IHa; clear IHa. apply less_succ_cancel. destruct H. apply (less_transitive (succ a) a (succ a)). exact H. apply less_succ. simpl. tauto. Defined. Lemma less_asymmetric (a b : N) : a < b -> b < a -> False. Proof. intros. apply (less_irreflexive a). apply (less_transitive a b a). exact H. exact H0. Defined. Theorem succ_cancel (a b : N) : succ a = succ b -> a = b. Proof. intro. assert (a < succ b). apply less_succ_cancel. rewrite -> H. apply less_succ. assert (b < succ a). apply less_succ_cancel. rewrite <- H. apply less_succ. clear H. simpl in H0. simpl in H1. destruct H0. destruct H1. absurd (b < a). unfold not. apply less_asymmetric. exact H. exact H0. symmetry; exact H0. exact H. Defined. Theorem add_cancel (a b c : N) : a + b = a + c -> b = c. Proof. induction a. simpl. tauto. intro. apply IHa. rewrite add_succ_l in H. rewrite add_succ_l in H. apply succ_cancel. exact H. Defined. Notation "a <= b" := (a = b \/ a < b). Lemma zero_smallest (a : N) : a <= zero -> a = zero. Proof. simpl. tauto. Defined. Lemma leq_succ (a b : N) : a <= succ b -> a = succ b \/ a <= b. Proof. simpl. tauto. Defined.