proposition: Lemma le_bool_ok_true : forall n m, le_bool n m = true -> le n m.
proof: Proof. induction n. intros m _;induction m. constructor. constructor;exact IHm. intros [|m]. intros abs;discriminate abs. simpl;intros h. apply le_n_S. apply IHn. exact h. Qed.
imports: Coq(Arith)