proposition: Lemma gt_double_n_S : forall a b : nat, a > b -> a + a > S (b + b).
proof: Proof. simple induction a. intros. absurd (0 > b). auto with arith. exact H. simple induction b. simpl in |- *. intro. apply gt_n_S. unfold gt in |- *. unfold lt in |- *. elim plus_n_Sm. auto with arith. intros. simpl in |- *. apply gt_n_S. elim plus_n_Sm. apply gt_n_S. elim plus_n_Sm. apply H. apply gt_S_n. exact H1. Qed.
imports: Plus Mult Minus Lt Le Gt