proposition: Theorem sorted_ins : forall (n : nat) (x : list nat), sorted x -> sorted (ins n x).
proof: Proof. simple induction x. trivial. intros. rewrite ins_eq2. apply si_intro. intros. rewrite sorted_eq3. split. assumption. assumption. intro. apply sorted_ins_Cons. assumption. assumption. Qed.