+lemma sorted_to_eq_sorted_b_true :
+ \forall A,ord,ordb.
+ (\forall x,y.ord x y \to ordb x y = true) \to
+ \forall l.sorted A ord l \to ordered A ordb l = true.
+intros 5;elim l
+ [reflexivity
+ |simplify;rewrite > H1;generalize in match H2;cases l1;intros
+ [reflexivity
+ |simplify;rewrite > H
+ [reflexivity
+ |apply (sorted_to_minimum ? ? ? ? H3);apply in_list_head]
+ |apply sort_nil
+ |apply (sorted_cons_to_sorted ? ? ? ? H3)]]
+qed.
+
+(*
+ TODO
+ per far funzionare questa dimostrazione bisogna appoggiarsi a un
+ eqb (e utilizzare quindi in_list <-> mem), oppure modificare la definizione
+ di sorted in modo che non si appoggi più a in_list:
+ sorted []
+ sorted [x] per ogni x
+ sorted x::y::l se ord x y e sorted y::l
+
+lemma eq_sorted_b_true_to_sorted :
+ \forall A,ord,ordb.
+ (\forall x,y.ordb x y = true \to ord x y) \to
+ \forall l.ordered A ordb l = true \to sorted A ord l.
+intros 5;elim l
+ [apply sort_nil
+ |apply sort_cons
+ [apply H1;simplify in H2;generalize in match H2;cases l1;intros
+ [reflexivity
+ |simplify in H3;simplify;apply (andb_true_true_r ? ? H3)]
+ |intros;apply H;generalize in match H2;
+ generalize in match (in_list_to_mem_true ? ? ? ? H
+ [
+*)
+
+let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝