proposition: Theorem bicycle_eq_seats' : forall x1 y1:nat, bicycle x1 = bicycle y1 -> x1 = y1.
proof: Proof. intros x1 y1 H. change (nb_seats (bicycle x1) = nb_seats (bicycle y1)). rewrite H; reflexivity. Qed.
imports: ZArith List Arith Bool