proposition: Lemma bubble_eq3 : forall (n m : nat) (x : list nat), bubble (Cons nat n (Cons nat m x)) = si (list nat) (inf_egal n m) (Cons nat n (bubble (Cons nat m x))) (Cons nat m (bubble (Cons nat n x))).
proof: Proof. auto. Qed.