proposition: Theorem sorted_ins_Cons : forall (x : list nat) (n m : nat), inf_egal n m = false -> sorted (Cons nat m x) -> sorted (Cons nat m (ins n x)).
proof: Proof. simple induction x. intros. rewrite ins_eq1. rewrite sorted_eq3. split. apply inf_false_true. assumption. trivial. intros. rewrite ins_eq2. apply (si_intro (list nat) (fun x : list nat => sorted (Cons nat m x))). intro. rewrite sorted_eq3. split. apply inf_false_true. assumption. rewrite sorted_eq3. split. apply H2. apply (sorted_cdr m). assumption. intro. rewrite sorted_eq3. split. apply (sorted_inf m x0 l). assumption. apply H. assumption. apply (sorted_cdr m). assumption. Qed.